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

Theorem syldan 280
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 115 . . 3 (𝜒 → (𝜑𝜃))
43adantrd 277 . 2 (𝜒 → ((𝜑𝜓) → 𝜃))
51, 4mpcom 36 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107
This theorem is referenced by:  sylan2  284  dn1dc  945  stoic2a  1406  sbcied2  2947  csbied2  3048  elpw2g  4085  pofun  4238  tfi  4500  fnbr  5229  caovlem2d  5967  grprinvlem  5969  caofcom  6009  fnexALT  6015  tfr1onlemres  6250  tfrcllemres  6263  tfri3  6268  ixpexgg  6620  f1domg  6656  fundmfi  6830  f1ofi  6835  archnqq  7245  nqpru  7380  ltaddpr  7425  1idsr  7596  addgt0sr  7603  suplocsrlempr  7635  gt0ap0  8408  ap0gt0  8422  mulgt1  8641  gt0div  8648  ge0div  8649  ltdiv2  8665  creur  8737  avgle1  8980  recnz  9164  qreccl  9457  xrrege0  9634  peano2fzor  10036  flqltnz  10087  flqdiv  10121  zmodcl  10144  frecuzrdgtcl  10212  frecuzrdgfunlem  10219  seq3fveq  10271  ser3mono  10278  iseqf1olemkle  10284  seq3f1olemqsumkj  10298  seq3f1olemqsumk  10299  seq3id  10308  seq3z  10311  le2sq2  10395  bcpasc  10540  fihasheqf1oi  10562  seq3coll  10613  caucvgrelemcau  10780  caucvgre  10781  r19.2uz  10793  sqrtgt0  10834  xrmaxiflemval  11047  clim2ser  11134  clim2ser2  11135  climub  11141  serf0  11149  fsumf1o  11187  fisumss  11189  fsumcl2lem  11195  fsumsplit  11204  fsum2dlemstep  11231  fisumrev2  11243  fsumlessfi  11257  telfsumo  11263  fsumparts  11267  fsumiun  11274  binom1dif  11284  isumsplit  11288  isumrpcl  11291  isumlessdc  11293  explecnv  11302  cvgratnnlemmn  11322  cvgratz  11329  cvgratgt0  11330  mertenslemi1  11332  clim2prod  11336  clim2divap  11337  ef0lem  11394  eftlub  11424  tanval3ap  11448  dvdssubr  11566  divalgmod  11651  divgcdnn  11690  algfx  11760  eucalgcvga  11766  lcmcllem  11775  lcmneg  11782  isprm6  11852  cncongrprm  11862  phimullem  11928  tgcl  12263  tgclb  12264  tgss2  12278  ntrss3  12322  ntridm  12325  opnssneib  12355  ssnei2  12356  innei  12362  resttopon  12370  cnpnei  12418  cnntri  12423  lmss  12445  txcnp  12470  blpnfctr  12638  mopni2  12682  bdmopn  12703  climcncf  12770  ivthdec  12821  cnplimcim  12835  dvconst  12860  dvef  12887  rpcxpneg  13027  abscxp  13034  cvgcmp2nlemabs  13385  trilpolemisumle  13389  trilpolemeq1  13391  trilpolemlt1  13392  neapmkvlem  13407
  Copyright terms: Public domain W3C validator