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  960  stoic2a  1429  sbcied2  3000  csbied2  3104  elpw2g  4154  pofun  4310  tfi  4579  fnbr  5315  caovlem2d  6062  caofcom  6101  fnexALT  6107  tfr1onlemres  6345  tfrcllemres  6358  tfri3  6363  ixpexgg  6717  f1domg  6753  fundmfi  6932  f1ofi  6937  archnqq  7411  nqpru  7546  ltaddpr  7591  1idsr  7762  addgt0sr  7769  suplocsrlempr  7801  gt0ap0  8577  ap0gt0  8591  mulgt1  8814  gt0div  8821  ge0div  8822  ltdiv2  8838  creur  8910  avgle1  9153  recnz  9340  qreccl  9636  xrrege0  9819  peano2fzor  10225  flqltnz  10280  flqdiv  10314  zmodcl  10337  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  seq3fveq  10464  ser3mono  10471  iseqf1olemkle  10477  seq3f1olemqsumkj  10491  seq3f1olemqsumk  10492  seq3id  10501  seq3z  10504  le2sq2  10588  bcpasc  10737  fihasheqf1oi  10758  seq3coll  10813  caucvgrelemcau  10980  caucvgre  10981  r19.2uz  10993  sqrtgt0  11034  xrmaxiflemval  11249  clim2ser  11336  clim2ser2  11337  climub  11343  serf0  11351  fsumf1o  11389  fisumss  11391  fsumcl2lem  11397  fsumsplit  11406  fsum2dlemstep  11433  fisumrev2  11445  fsumlessfi  11459  telfsumo  11465  fsumparts  11469  fsumiun  11476  binom1dif  11486  isumsplit  11490  isumrpcl  11493  isumlessdc  11495  explecnv  11504  cvgratnnlemmn  11524  cvgratz  11531  cvgratgt0  11532  mertenslemi1  11534  clim2prod  11538  clim2divap  11539  fprodseq  11582  fprodf1o  11587  prodssdc  11588  fprodssdc  11589  fprodsplitdc  11595  fprodeq0  11616  fprod2dlemstep  11621  ef0lem  11659  eftlub  11689  tanval3ap  11713  dvdssubr  11837  divalgmod  11922  divgcdnn  11966  algfx  12042  eucalgcvga  12048  lcmcllem  12057  lcmneg  12064  isprm6  12137  cncongrprm  12147  phimullem  12215  pcid  12313  pcgcd  12318  pcz  12321  4sqlem9  12374  grpidd  12732  ismndd  12768  grpinvid1  12852  grpinvid2  12853  grplcan  12860  grpinvinv  12865  grpinvval2  12881  mulgass  12947  mulgpropdg  12952  subginv  12967  subgmulg  12974  issubg2m  12975  issubg4m  12979  subsubg  12983  ringidss  13112  isringd  13120  ringlz  13122  ringrz  13123  unitgrp  13184  0unit  13197  unitnegcl  13198  dvrass  13207  dvreq1  13210  dvrdir  13211  ringinvdv  13213  invrpropdg  13217  tgcl  13346  tgclb  13347  tgss2  13361  ntrss3  13405  ntridm  13408  opnssneib  13438  ssnei2  13439  innei  13445  resttopon  13453  cnpnei  13501  cnntri  13506  lmss  13528  txcnp  13553  blpnfctr  13721  mopni2  13765  bdmopn  13786  climcncf  13853  ivthdec  13904  cnplimcim  13918  dvconst  13943  dvef  13970  rpcxpneg  14110  abscxp  14117  lgscllem  14190  lgsvalmod  14202  lgsdir2  14216  cvgcmp2nlemabs  14551  trilpolemisumle  14557  trilpolemeq1  14559  trilpolemlt1  14560  nconstwlpolemgt0  14582  neapmkvlem  14585