Theorem syldan 280

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 115	. . 3 |- ( ch -> ( ph -> th ) )
4	3	adantrd 277	. 2 |- ( ch -> ( ( ph /\ ps ) -> th ) )
5	1, 4	mpcom 36	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  sylan2  284  dn1dc  955  stoic2a  1422  sbcied2  2992  csbied2  3096  elpw2g  4142  pofun  4297  tfi  4566  fnbr  5300  caovlem2d  6045  caofcom  6084  fnexALT  6090  tfr1onlemres  6328  tfrcllemres  6341  tfri3  6346  ixpexgg  6700  f1domg  6736  fundmfi  6915  f1ofi  6920  archnqq  7379  nqpru  7514  ltaddpr  7559  1idsr  7730  addgt0sr  7737  suplocsrlempr  7769  gt0ap0  8545  ap0gt0  8559  mulgt1  8779  gt0div  8786  ge0div  8787  ltdiv2  8803  creur  8875  avgle1  9118  recnz  9305  qreccl  9601  xrrege0  9782  peano2fzor  10188  flqltnz  10243  flqdiv  10277  zmodcl  10300  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  seq3fveq  10427  ser3mono  10434  iseqf1olemkle  10440  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3id  10464  seq3z  10467  le2sq2  10551  bcpasc  10700  fihasheqf1oi  10722  seq3coll  10777  caucvgrelemcau  10944  caucvgre  10945  r19.2uz  10957  sqrtgt0  10998  xrmaxiflemval  11213  clim2ser  11300  clim2ser2  11301  climub  11307  serf0  11315  fsumf1o  11353  fisumss  11355  fsumcl2lem  11361  fsumsplit  11370  fsum2dlemstep  11397  fisumrev2  11409  fsumlessfi  11423  telfsumo  11429  fsumparts  11433  fsumiun  11440  binom1dif  11450  isumsplit  11454  isumrpcl  11457  isumlessdc  11459  explecnv  11468  cvgratnnlemmn  11488  cvgratz  11495  cvgratgt0  11496  mertenslemi1  11498  clim2prod  11502  clim2divap  11503  fprodseq  11546  fprodf1o  11551  prodssdc  11552  fprodssdc  11553  fprodsplitdc  11559  fprodeq0  11580  fprod2dlemstep  11585  ef0lem  11623  eftlub  11653  tanval3ap  11677  dvdssubr  11801  divalgmod  11886  divgcdnn  11930  algfx  12006  eucalgcvga  12012  lcmcllem  12021  lcmneg  12028  isprm6  12101  cncongrprm  12111  phimullem  12179  pcid  12277  pcgcd  12282  pcz  12285  4sqlem9  12338  grpidd  12637  ismndd  12673  grpinvid1  12754  grpinvid2  12755  grplcan  12761  grpinvinv  12766  tgcl  12858  tgclb  12859  tgss2  12873  ntrss3  12917  ntridm  12920  opnssneib  12950  ssnei2  12951  innei  12957  resttopon  12965  cnpnei  13013  cnntri  13018  lmss  13040  txcnp  13065  blpnfctr  13233  mopni2  13277  bdmopn  13298  climcncf  13365  ivthdec  13416  cnplimcim  13430  dvconst  13455  dvef  13482  rpcxpneg  13622  abscxp  13629  lgscllem  13702  lgsvalmod  13714  lgsdir2  13728  cvgcmp2nlemabs  14064  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  nconstwlpolemgt0  14095  neapmkvlem  14098