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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is used by:  sylan2  286  dn1dc  973  stoic2a  1478  sbcied2  3089  csbied2  3195  elpw2g  4292  pofun  4457  tfi  4729  fnbr  5485  caovlem2d  6282  caofcom  6333  fnexALT  6340  elabreximd  6356  tfr1onlemres  6620  tfrcllemres  6633  tfri3  6638  ixpexgg  7004  f1domg  7044  fundmfi  7251  f1ofi  7257  finacn  7560  archnqq  7784  nqpru  7919  ltaddpr  7964  1idsr  8135  addgt0sr  8142  suplocsrlempr  8174  gt0ap0  8956  ap0gt0  8970  mulgt1  9195  gt0div  9202  ge0div  9203  ltdiv2  9219  creur  9291  avgle1  9550  recnz  9743  qreccl  10051  xrrege0  10237  peano2fzor  10660  flqltnz  10735  flqdiv  10771  zmodcl  10794  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  seqfveqg  10928  seq3fveq  10929  ser3mono  10937  seqsplitg  10939  seqcaopr2g  10944  iseqf1olemkle  10947  seq3f1olemqsumkj  10961  seq3f1olemqsumk  10962  seqf1oglem2  10970  seqf1og  10971  seq3id  10975  seq3z  10978  seqhomog  10980  le2sq2  11065  bcpasc  11218  fihasheqf1oi  11240  seq3coll  11308  wrdnval  11349  wrdsymb1  11355  lswcl  11369  ccatlid  11388  ccatass  11390  ccat1st1st  11423  lswccats1fst  11426  swrdlsw  11455  ccatswrd  11456  pfxtrcfvl  11483  pfxsuff1eqwrdeq  11485  ccatpfx  11487  pfx1  11489  pfxswrd  11492  pfxlswccat  11499  swrdccatin2  11515  pfxccatin12  11519  caucvgrelemcau  11760  caucvgre  11761  r19.2uz  11773  sqrtgt0  11814  xrmaxiflemval  12032  clim2ser  12119  clim2ser2  12120  climub  12126  serf0  12134  fsumf1o  12173  fisumss  12175  fsumcl2lem  12181  fsumsplit  12190  fsum2dlemstep  12217  fisumrev2  12229  fsumlessfi  12243  telfsumo  12249  fsumparts  12253  fsumiun  12260  binom1dif  12270  isumsplit  12274  isumrpcl  12277  isumlessdc  12279  explecnv  12288  cvgratnnlemmn  12308  cvgratz  12315  cvgratgt0  12316  mertenslemi1  12318  clim2prod  12322  clim2divap  12323  fprodseq  12366  fprodf1o  12371  prodssdc  12372  fprodssdc  12373  fprodsplitdc  12379  fprodeq0  12400  fprod2dlemstep  12405  ef0lem  12443  eftlub  12473  tanval3ap  12497  dvdssubr  12622  divalgmod  12710  bitsdc  12730  bitsp1  12734  divgcdnn  12768  algfx  12846  eucalgcvga  12852  lcmcllem  12861  lcmneg  12868  isprm6  12942  cncongrprm  12952  nn0sqdcq  13004  phimullem  13023  pcid  13123  pcgcd  13128  pcz  13131  4sqlem9  13185  4sqlem15  13204  4sqlem16  13205  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemsel1i  13305  ballotfilemsima  13308  ballotfilemfrceq  13321  imasex  13675  grpidd  13752  gzsumress  13761  ismndd  13799  subsubm  13839  grpinvid1  13906  grpinvid2  13907  grplcan  13916  grpinvinv  13921  grpinvval2  13937  mulgass  14011  mulgpropdg  14016  subginv  14033  subgmulg  14040  issubg2m  14041  issubg4m  14045  subsubg  14049  eqger  14076  qusinv  14088  resghm  14112  conjsubgen  14130  rngrz  14294  isrngd  14301  ringidss  14383  isringd  14395  ringlz  14397  ringrz  14398  unitgrp  14472  0unit  14485  unitnegcl  14486  dvrass  14495  dvreq1  14498  dvrdir  14499  ringinvdv  14501  invrpropdg  14505  rhmunitinv  14534  issubrng2  14567  subsubrng  14571  subrg1  14588  issubrg2  14598  subsubrg  14602  lmod0vs  14707  lmodvs0  14708  lmodvneg1  14716  islss3  14765  lspsnsubg  14782  lspid  14783  lspssv  14784  lspidm  14787  lspsnneg  14806  sraval  14823  qus1  14912  zringmulg  14982  mulgrhm  14993  znidom  15041  issubassa3  15061  tgcl  15214  tgclb  15215  tgss2  15229  ntrss3  15273  ntridm  15276  opnssneib  15306  ssnei2  15307  innei  15313  resttopon  15321  cnpnei  15369  cnntri  15374  lmss  15396  txcnp  15421  blpnfctr  15589  mopni2  15633  bdmopn  15654  climcncf  15734  ivthdec  15794  cnplimcim  15817  dvconst  15844  dvconstre  15846  dvef  15877  plymullem  15900  plycoeid3  15907  rpcxpneg  16062  abscxp  16070  log2tlbndlog2  16139  birthdaylem2  16145  ppiqsval  16156  ppiprm  16170  ppiqltx  16183  sgmmul  16191  bposlem3  16211  lgscllem  16224  lgsvalmod  16236  lgsdir2  16250  lgsquadlem2  16295  lgsquad2lem2  16299  upgredg  16483  usgruspgrben  16525  usgredg3  16553  cvgcmp2nlemabs  17179  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  nconstwlpolemgt0  17212  neapmkvlem  17215