Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syldan GIF version

Theorem syldan 266
 Description: A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
Hypotheses
Ref Expression
syldan.1 ((𝜑𝜓) → 𝜒)
syldan.2 ((𝜑𝜒) → 𝜃)
Assertion
Ref Expression
syldan ((𝜑𝜓) → 𝜃)

Proof of Theorem syldan
StepHypRef Expression
1 syldan.1 . 2 ((𝜑𝜓) → 𝜒)
2 syldan.2 . . . 4 ((𝜑𝜒) → 𝜃)
32expcom 109 . . 3 (𝜒 → (𝜑𝜃))
43adantrd 264 . 2 (𝜒 → ((𝜑𝜓) → 𝜃))
51, 4mpcom 32 1 ((𝜑𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia3 101 This theorem is referenced by:  sylan2  270  dn1dc  867  stoic2a  1318  sbcied2  2800  csbied2  2893  elpw2g  3910  pofun  4049  tfi  4305  fnbr  5001  caovlem2d  5693  grprinvlem  5695  caofcom  5734  fnexALT  5740  tfri3  5953  f1domg  6238  archnqq  6515  nqpru  6650  ltaddpr  6695  1idsr  6853  addgt0sr  6860  gt0ap0  7616  ap0gt0  7629  mulgt1  7829  gt0div  7836  ge0div  7837  ltdiv2  7853  creur  7911  avgle1  8165  recnz  8333  qreccl  8576  xrrege0  8738  peano2fzor  9088  flqltnz  9129  flqdiv  9163  frecuzrdgfn  9198  frecuzrdgcl  9199  frecuzrdgsuc  9201  iseqfveq  9230  isermono  9237  iseqsplit  9238  iseqid  9247  le2sq2  9329  caucvgrelemcau  9579  caucvgre  9580  r19.2uz  9591  sqrtgt0  9632  clim2iser  9857  clim2iser2  9858  climub  9864  serif0  9871  ialgfx  9891
 Copyright terms: Public domain W3C validator