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  966  stoic2a  1471  sbcied2  3066  csbied2  3172  elpw2g  4240  pofun  4403  tfi  4674  fnbr  5425  caovlem2d  6198  caofcom  6249  fnexALT  6256  tfr1onlemres  6495  tfrcllemres  6508  tfri3  6513  ixpexgg  6869  f1domg  6909  fundmfi  7104  f1ofi  7110  finacn  7386  archnqq  7604  nqpru  7739  ltaddpr  7784  1idsr  7955  addgt0sr  7962  suplocsrlempr  7994  gt0ap0  8773  ap0gt0  8787  mulgt1  9010  gt0div  9017  ge0div  9018  ltdiv2  9034  creur  9106  avgle1  9352  recnz  9540  qreccl  9837  xrrege0  10021  peano2fzor  10438  flqltnz  10507  flqdiv  10543  zmodcl  10566  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  seqfveqg  10700  seq3fveq  10701  ser3mono  10709  seqsplitg  10711  seqcaopr2g  10716  iseqf1olemkle  10719  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seqf1oglem2  10742  seqf1og  10743  seq3id  10747  seq3z  10750  seqhomog  10752  le2sq2  10837  bcpasc  10988  fihasheqf1oi  11009  seq3coll  11064  wrdnval  11102  wrdsymb1  11108  lswcl  11122  ccatlid  11141  ccatass  11143  ccat1st1st  11172  lswccats1fst  11175  swrdlsw  11201  ccatswrd  11202  pfxtrcfvl  11229  pfxsuff1eqwrdeq  11231  ccatpfx  11233  pfx1  11235  pfxswrd  11238  pfxlswccat  11245  swrdccatin2  11261  pfxccatin12  11265  caucvgrelemcau  11491  caucvgre  11492  r19.2uz  11504  sqrtgt0  11545  xrmaxiflemval  11761  clim2ser  11848  clim2ser2  11849  climub  11855  serf0  11863  fsumf1o  11901  fisumss  11903  fsumcl2lem  11909  fsumsplit  11918  fsum2dlemstep  11945  fisumrev2  11957  fsumlessfi  11971  telfsumo  11977  fsumparts  11981  fsumiun  11988  binom1dif  11998  isumsplit  12002  isumrpcl  12005  isumlessdc  12007  explecnv  12016  cvgratnnlemmn  12036  cvgratz  12043  cvgratgt0  12044  mertenslemi1  12046  clim2prod  12050  clim2divap  12051  fprodseq  12094  fprodf1o  12099  prodssdc  12100  fprodssdc  12101  fprodsplitdc  12107  fprodeq0  12128  fprod2dlemstep  12133  ef0lem  12171  eftlub  12201  tanval3ap  12225  dvdssubr  12350  divalgmod  12438  bitsdc  12458  bitsp1  12462  divgcdnn  12496  algfx  12574  eucalgcvga  12580  lcmcllem  12589  lcmneg  12596  isprm6  12669  cncongrprm  12679  phimullem  12747  pcid  12847  pcgcd  12852  pcz  12855  4sqlem9  12909  4sqlem15  12928  4sqlem16  12929  imasex  13338  grpidd  13416  gsumress  13428  ismndd  13470  subsubm  13516  grpinvid1  13585  grpinvid2  13586  grplcan  13595  grpinvinv  13600  grpinvval2  13616  mulgass  13696  mulgpropdg  13701  subginv  13718  subgmulg  13725  issubg2m  13726  issubg4m  13730  subsubg  13734  eqger  13761  qusinv  13773  resghm  13797  conjsubgen  13815  rngrz  13909  isrngd  13916  ringidss  13992  isringd  14004  ringlz  14006  ringrz  14007  unitgrp  14080  0unit  14093  unitnegcl  14094  dvrass  14103  dvreq1  14106  dvrdir  14107  ringinvdv  14109  invrpropdg  14113  rhmunitinv  14142  issubrng2  14174  subsubrng  14178  subrg1  14195  issubrg2  14205  subsubrg  14209  lmod0vs  14285  lmodvs0  14286  lmodvneg1  14294  islss3  14343  lspsnsubg  14360  lspid  14361  lspssv  14362  lspidm  14365  lspsnneg  14384  sraval  14401  qus1  14490  zringmulg  14562  mulgrhm  14573  znidom  14621  tgcl  14738  tgclb  14739  tgss2  14753  ntrss3  14797  ntridm  14800  opnssneib  14830  ssnei2  14831  innei  14837  resttopon  14845  cnpnei  14893  cnntri  14898  lmss  14920  txcnp  14945  blpnfctr  15113  mopni2  15157  bdmopn  15178  climcncf  15258  ivthdec  15318  cnplimcim  15341  dvconst  15368  dvconstre  15370  dvef  15401  plymullem  15424  plycoeid3  15431  rpcxpneg  15581  abscxp  15589  sgmmul  15670  lgscllem  15686  lgsvalmod  15698  lgsdir2  15712  lgsquadlem2  15757  lgsquad2lem2  15761  upgredg  15942  usgruspgrben  15984  usgredg3  16012  cvgcmp2nlemabs  16400  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  nconstwlpolemgt0  16432  neapmkvlem  16435