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  4190  pofun  4348  tfi  4619  fnbr  5363  caovlem2d  6120  caofcom  6170  fnexALT  6177  tfr1onlemres  6416  tfrcllemres  6429  tfri3  6434  ixpexgg  6790  f1domg  6826  fundmfi  7012  f1ofi  7018  finacn  7289  archnqq  7503  nqpru  7638  ltaddpr  7683  1idsr  7854  addgt0sr  7861  suplocsrlempr  7893  gt0ap0  8672  ap0gt0  8686  mulgt1  8909  gt0div  8916  ge0div  8917  ltdiv2  8933  creur  9005  avgle1  9251  recnz  9438  qreccl  9735  xrrege0  9919  peano2fzor  10327  flqltnz  10396  flqdiv  10432  zmodcl  10455  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  seqfveqg  10589  seq3fveq  10590  ser3mono  10598  seqsplitg  10600  seqcaopr2g  10605  iseqf1olemkle  10608  seq3f1olemqsumkj  10622  seq3f1olemqsumk  10623  seqf1oglem2  10631  seqf1og  10632  seq3id  10636  seq3z  10639  seqhomog  10641  le2sq2  10726  bcpasc  10877  fihasheqf1oi  10898  seq3coll  10953  wrdnval  10984  wrdsymb1  10990  caucvgrelemcau  11164  caucvgre  11165  r19.2uz  11177  sqrtgt0  11218  xrmaxiflemval  11434  clim2ser  11521  clim2ser2  11522  climub  11528  serf0  11536  fsumf1o  11574  fisumss  11576  fsumcl2lem  11582  fsumsplit  11591  fsum2dlemstep  11618  fisumrev2  11630  fsumlessfi  11644  telfsumo  11650  fsumparts  11654  fsumiun  11661  binom1dif  11671  isumsplit  11675  isumrpcl  11678  isumlessdc  11680  explecnv  11689  cvgratnnlemmn  11709  cvgratz  11716  cvgratgt0  11717  mertenslemi1  11719  clim2prod  11723  clim2divap  11724  fprodseq  11767  fprodf1o  11772  prodssdc  11773  fprodssdc  11774  fprodsplitdc  11780  fprodeq0  11801  fprod2dlemstep  11806  ef0lem  11844  eftlub  11874  tanval3ap  11898  dvdssubr  12023  divalgmod  12111  bitsdc  12131  bitsp1  12135  divgcdnn  12169  algfx  12247  eucalgcvga  12253  lcmcllem  12262  lcmneg  12269  isprm6  12342  cncongrprm  12352  phimullem  12420  pcid  12520  pcgcd  12525  pcz  12528  4sqlem9  12582  4sqlem15  12601  4sqlem16  12602  imasex  13009  grpidd  13087  gsumress  13099  ismndd  13141  subsubm  13187  grpinvid1  13256  grpinvid2  13257  grplcan  13266  grpinvinv  13271  grpinvval2  13287  mulgass  13367  mulgpropdg  13372  subginv  13389  subgmulg  13396  issubg2m  13397  issubg4m  13401  subsubg  13405  eqger  13432  qusinv  13444  resghm  13468  conjsubgen  13486  rngrz  13580  isrngd  13587  ringidss  13663  isringd  13675  ringlz  13677  ringrz  13678  unitgrp  13750  0unit  13763  unitnegcl  13764  dvrass  13773  dvreq1  13776  dvrdir  13777  ringinvdv  13779  invrpropdg  13783  rhmunitinv  13812  issubrng2  13844  subsubrng  13848  subrg1  13865  issubrg2  13875  subsubrg  13879  lmod0vs  13955  lmodvs0  13956  lmodvneg1  13964  islss3  14013  lspsnsubg  14030  lspid  14031  lspssv  14032  lspidm  14035  lspsnneg  14054  sraval  14071  qus1  14160  zringmulg  14232  mulgrhm  14243  znidom  14291  tgcl  14408  tgclb  14409  tgss2  14423  ntrss3  14467  ntridm  14470  opnssneib  14500  ssnei2  14501  innei  14507  resttopon  14515  cnpnei  14563  cnntri  14568  lmss  14590  txcnp  14615  blpnfctr  14783  mopni2  14827  bdmopn  14848  climcncf  14928  ivthdec  14988  cnplimcim  15011  dvconst  15038  dvconstre  15040  dvef  15071  plymullem  15094  plycoeid3  15101  rpcxpneg  15251  abscxp  15259  sgmmul  15340  lgscllem  15356  lgsvalmod  15368  lgsdir2  15382  lgsquadlem2  15427  lgsquad2lem2  15431  cvgcmp2nlemabs  15789  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  nconstwlpolemgt0  15821  neapmkvlem  15824