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  950  stoic2a  1417  sbcied2  2988  csbied2  3092  elpw2g  4135  pofun  4290  tfi  4559  fnbr  5290  caovlem2d  6034  caofcom  6073  fnexALT  6079  tfr1onlemres  6317  tfrcllemres  6330  tfri3  6335  ixpexgg  6688  f1domg  6724  fundmfi  6903  f1ofi  6908  archnqq  7358  nqpru  7493  ltaddpr  7538  1idsr  7709  addgt0sr  7716  suplocsrlempr  7748  gt0ap0  8524  ap0gt0  8538  mulgt1  8758  gt0div  8765  ge0div  8766  ltdiv2  8782  creur  8854  avgle1  9097  recnz  9284  qreccl  9580  xrrege0  9761  peano2fzor  10167  flqltnz  10222  flqdiv  10256  zmodcl  10279  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  seq3fveq  10406  ser3mono  10413  iseqf1olemkle  10419  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3id  10443  seq3z  10446  le2sq2  10530  bcpasc  10679  fihasheqf1oi  10701  seq3coll  10755  caucvgrelemcau  10922  caucvgre  10923  r19.2uz  10935  sqrtgt0  10976  xrmaxiflemval  11191  clim2ser  11278  clim2ser2  11279  climub  11285  serf0  11293  fsumf1o  11331  fisumss  11333  fsumcl2lem  11339  fsumsplit  11348  fsum2dlemstep  11375  fisumrev2  11387  fsumlessfi  11401  telfsumo  11407  fsumparts  11411  fsumiun  11418  binom1dif  11428  isumsplit  11432  isumrpcl  11435  isumlessdc  11437  explecnv  11446  cvgratnnlemmn  11466  cvgratz  11473  cvgratgt0  11474  mertenslemi1  11476  clim2prod  11480  clim2divap  11481  fprodseq  11524  fprodf1o  11529  prodssdc  11530  fprodssdc  11531  fprodsplitdc  11537  fprodeq0  11558  fprod2dlemstep  11563  ef0lem  11601  eftlub  11631  tanval3ap  11655  dvdssubr  11779  divalgmod  11864  divgcdnn  11908  algfx  11984  eucalgcvga  11990  lcmcllem  11999  lcmneg  12006  isprm6  12079  cncongrprm  12089  phimullem  12157  pcid  12255  pcgcd  12260  pcz  12263  4sqlem9  12316  grpidd  12614  tgcl  12704  tgclb  12705  tgss2  12719  ntrss3  12763  ntridm  12766  opnssneib  12796  ssnei2  12797  innei  12803  resttopon  12811  cnpnei  12859  cnntri  12864  lmss  12886  txcnp  12911  blpnfctr  13079  mopni2  13123  bdmopn  13144  climcncf  13211  ivthdec  13262  cnplimcim  13276  dvconst  13301  dvef  13328  rpcxpneg  13468  abscxp  13475  lgscllem  13548  lgsvalmod  13560  lgsdir2  13574  cvgcmp2nlemabs  13911  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  nconstwlpolemgt0  13942  neapmkvlem  13945