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

Theorem syldan 270
 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 113 . . 3 (𝜒 → (𝜑𝜃))
43adantrd 268 . 2 (𝜒 → ((𝜑𝜓) → 𝜃))
51, 4mpcom 36 1 ((𝜑𝜓) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia3 105 This theorem is referenced by:  sylan2  274  dn1dc  878  stoic2a  1334  sbcied2  2822  csbied2  2920  elpw2g  3937  pofun  4076  tfi  4332  fnbr  5028  caovlem2d  5720  grprinvlem  5722  caofcom  5761  fnexALT  5767  tfri3  5983  f1domg  6268  archnqq  6572  nqpru  6707  ltaddpr  6752  1idsr  6910  addgt0sr  6917  gt0ap0  7689  ap0gt0  7702  mulgt1  7903  gt0div  7910  ge0div  7911  ltdiv2  7927  creur  7986  avgle1  8221  recnz  8390  qreccl  8673  xrrege0  8838  peano2fzor  9189  flqltnz  9236  flqdiv  9270  zmodcl  9293  frecuzrdgfn  9361  frecuzrdgcl  9362  frecuzrdgsuc  9364  iseqfveq  9393  isermono  9400  iseqsplit  9401  iseqid  9410  iseqz  9412  le2sq2  9494  bcpasc  9633  caucvgrelemcau  9806  caucvgre  9807  r19.2uz  9819  sqrtgt0  9860  clim2iser  10087  clim2iser2  10088  climub  10094  serif0  10101  dvdssubr  10152  ialgfx  10253
 Copyright terms: Public domain W3C validator