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  962  stoic2a  1440  sbcied2  3027  csbied2  3132  elpw2g  4189  pofun  4347  tfi  4618  fnbr  5360  caovlem2d  6116  caofcom  6161  fnexALT  6168  tfr1onlemres  6407  tfrcllemres  6420  tfri3  6425  ixpexgg  6781  f1domg  6817  fundmfi  7003  f1ofi  7009  archnqq  7484  nqpru  7619  ltaddpr  7664  1idsr  7835  addgt0sr  7842  suplocsrlempr  7874  gt0ap0  8653  ap0gt0  8667  mulgt1  8890  gt0div  8897  ge0div  8898  ltdiv2  8914  creur  8986  avgle1  9232  recnz  9419  qreccl  9716  xrrege0  9900  peano2fzor  10308  flqltnz  10377  flqdiv  10413  zmodcl  10436  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  seqfveqg  10570  seq3fveq  10571  ser3mono  10579  seqsplitg  10581  seqcaopr2g  10586  iseqf1olemkle  10589  seq3f1olemqsumkj  10603  seq3f1olemqsumk  10604  seqf1oglem2  10612  seqf1og  10613  seq3id  10617  seq3z  10620  seqhomog  10622  le2sq2  10707  bcpasc  10858  fihasheqf1oi  10879  seq3coll  10934  wrdnval  10965  wrdsymb1  10971  caucvgrelemcau  11145  caucvgre  11146  r19.2uz  11158  sqrtgt0  11199  xrmaxiflemval  11415  clim2ser  11502  clim2ser2  11503  climub  11509  serf0  11517  fsumf1o  11555  fisumss  11557  fsumcl2lem  11563  fsumsplit  11572  fsum2dlemstep  11599  fisumrev2  11611  fsumlessfi  11625  telfsumo  11631  fsumparts  11635  fsumiun  11642  binom1dif  11652  isumsplit  11656  isumrpcl  11659  isumlessdc  11661  explecnv  11670  cvgratnnlemmn  11690  cvgratz  11697  cvgratgt0  11698  mertenslemi1  11700  clim2prod  11704  clim2divap  11705  fprodseq  11748  fprodf1o  11753  prodssdc  11754  fprodssdc  11755  fprodsplitdc  11761  fprodeq0  11782  fprod2dlemstep  11787  ef0lem  11825  eftlub  11855  tanval3ap  11879  dvdssubr  12004  divalgmod  12092  bitsp1  12115  divgcdnn  12142  algfx  12220  eucalgcvga  12226  lcmcllem  12235  lcmneg  12242  isprm6  12315  cncongrprm  12325  phimullem  12393  pcid  12493  pcgcd  12498  pcz  12501  4sqlem9  12555  4sqlem15  12574  4sqlem16  12575  imasex  12948  grpidd  13026  gsumress  13038  ismndd  13078  subsubm  13115  grpinvid1  13184  grpinvid2  13185  grplcan  13194  grpinvinv  13199  grpinvval2  13215  mulgass  13289  mulgpropdg  13294  subginv  13311  subgmulg  13318  issubg2m  13319  issubg4m  13323  subsubg  13327  eqger  13354  qusinv  13366  resghm  13390  conjsubgen  13408  rngrz  13502  isrngd  13509  ringidss  13585  isringd  13597  ringlz  13599  ringrz  13600  unitgrp  13672  0unit  13685  unitnegcl  13686  dvrass  13695  dvreq1  13698  dvrdir  13699  ringinvdv  13701  invrpropdg  13705  rhmunitinv  13734  issubrng2  13766  subsubrng  13770  subrg1  13787  issubrg2  13797  subsubrg  13801  lmod0vs  13877  lmodvs0  13878  lmodvneg1  13886  islss3  13935  lspsnsubg  13952  lspid  13953  lspssv  13954  lspidm  13957  lspsnneg  13976  sraval  13993  qus1  14082  zringmulg  14154  mulgrhm  14165  znidom  14213  tgcl  14300  tgclb  14301  tgss2  14315  ntrss3  14359  ntridm  14362  opnssneib  14392  ssnei2  14393  innei  14399  resttopon  14407  cnpnei  14455  cnntri  14460  lmss  14482  txcnp  14507  blpnfctr  14675  mopni2  14719  bdmopn  14740  climcncf  14820  ivthdec  14880  cnplimcim  14903  dvconst  14930  dvconstre  14932  dvef  14963  plymullem  14986  plycoeid3  14993  rpcxpneg  15143  abscxp  15151  sgmmul  15232  lgscllem  15248  lgsvalmod  15260  lgsdir2  15274  lgsquadlem2  15319  lgsquad2lem2  15323  cvgcmp2nlemabs  15676  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  nconstwlpolemgt0  15708  neapmkvlem  15711