Theorem syldan 282

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	|- ( ( ph /\ ps ) -> ch )
syldan.2	|- ( ( ph /\ ch ) -> th )

Assertion

Ref	Expression
syldan	|- ( ( ph /\ ps ) -> th )

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. 2 |- ( ( ph /\ ps ) -> ch )
2		syldan.2	. . . 4 |- ( ( ph /\ ch ) -> th )
3	2	expcom 116	. . 3 |- ( ch -> ( ph -> th ) )
4	3	adantrd 279	. 2 |- ( ch -> ( ( ph /\ ps ) -> th ) )
5	1, 4	mpcom 36	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is referenced by:  sylan2  286  dn1dc  960  stoic2a  1429  sbcied2  3001  csbied2  3105  elpw2g  4157  pofun  4313  tfi  4582  fnbr  5319  caovlem2d  6067  caofcom  6106  fnexALT  6112  tfr1onlemres  6350  tfrcllemres  6363  tfri3  6368  ixpexgg  6722  f1domg  6758  fundmfi  6937  f1ofi  6942  archnqq  7416  nqpru  7551  ltaddpr  7596  1idsr  7767  addgt0sr  7774  suplocsrlempr  7806  gt0ap0  8583  ap0gt0  8597  mulgt1  8820  gt0div  8827  ge0div  8828  ltdiv2  8844  creur  8916  avgle1  9159  recnz  9346  qreccl  9642  xrrege0  9825  peano2fzor  10232  flqltnz  10287  flqdiv  10321  zmodcl  10344  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  seq3fveq  10471  ser3mono  10478  iseqf1olemkle  10484  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3id  10508  seq3z  10511  le2sq2  10596  bcpasc  10746  fihasheqf1oi  10767  seq3coll  10822  caucvgrelemcau  10989  caucvgre  10990  r19.2uz  11002  sqrtgt0  11043  xrmaxiflemval  11258  clim2ser  11345  clim2ser2  11346  climub  11352  serf0  11360  fsumf1o  11398  fisumss  11400  fsumcl2lem  11406  fsumsplit  11415  fsum2dlemstep  11442  fisumrev2  11454  fsumlessfi  11468  telfsumo  11474  fsumparts  11478  fsumiun  11485  binom1dif  11495  isumsplit  11499  isumrpcl  11502  isumlessdc  11504  explecnv  11513  cvgratnnlemmn  11533  cvgratz  11540  cvgratgt0  11541  mertenslemi1  11543  clim2prod  11547  clim2divap  11548  fprodseq  11591  fprodf1o  11596  prodssdc  11597  fprodssdc  11598  fprodsplitdc  11604  fprodeq0  11625  fprod2dlemstep  11630  ef0lem  11668  eftlub  11698  tanval3ap  11722  dvdssubr  11846  divalgmod  11932  divgcdnn  11976  algfx  12052  eucalgcvga  12058  lcmcllem  12067  lcmneg  12074  isprm6  12147  cncongrprm  12157  phimullem  12225  pcid  12323  pcgcd  12328  pcz  12331  4sqlem9  12384  imasex  12726  grpidd  12802  ismndd  12838  grpinvid1  12924  grpinvid2  12925  grplcan  12932  grpinvinv  12937  grpinvval2  12953  mulgass  13020  mulgpropdg  13025  subginv  13041  subgmulg  13048  issubg2m  13049  issubg4m  13053  subsubg  13057  eqger  13083  ringidss  13212  isringd  13220  ringlz  13222  ringrz  13223  unitgrp  13285  0unit  13298  unitnegcl  13299  dvrass  13308  dvreq1  13311  dvrdir  13312  ringinvdv  13314  invrpropdg  13318  subrg1  13352  issubrg2  13362  subsubrg  13366  lmod0vs  13411  lmodvs0  13412  lmodvneg1  13420  zringmulg  13491  tgcl  13567  tgclb  13568  tgss2  13582  ntrss3  13626  ntridm  13629  opnssneib  13659  ssnei2  13660  innei  13666  resttopon  13674  cnpnei  13722  cnntri  13727  lmss  13749  txcnp  13774  blpnfctr  13942  mopni2  13986  bdmopn  14007  climcncf  14074  ivthdec  14125  cnplimcim  14139  dvconst  14164  dvef  14191  rpcxpneg  14331  abscxp  14338  lgscllem  14411  lgsvalmod  14423  lgsdir2  14437  cvgcmp2nlemabs  14783  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  nconstwlpolemgt0  14814  neapmkvlem  14817