Theorem syld3an3 1371

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

Ref	Expression
syld3an3.1	|- ( ( ph /\ ps /\ ch ) -> th )
syld3an3.2	|- ( ( ph /\ ps /\ th ) -> ta )

Assertion

Ref	Expression
syld3an3	|- ( ( ph /\ ps /\ ch ) -> ta )

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 1061	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2		simp2 1062	. 2 |- ( ( ph /\ ps /\ ch ) -> ps )
3		syld3an3.1	. 2 |- ( ( ph /\ ps /\ ch ) -> th )
4		syld3an3.2	. 2 |- ( ( ph /\ ps /\ th ) -> ta )
5	1, 2, 3, 4	syl3anc 1326	1 |- ( ( ph /\ ps /\ ch ) -> ta )

Syntax hints:   -> wi 4   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  syld3an1  1372  syld3an2  1373  brelrng  5355  resin  6158  moriotass  6640  omwordri  7652  oewordri  7672  gchaleph2  9494  gruf  9633  nnncan1  10317  lediv1  10888  lemuldiv  10903  suprfinzcl  11492  supxrbnd  12158  bcval4  13094  ccatval3  13363  ccatfv0  13367  ccatval1lsw  13368  lswccatn0lsw  13373  2swrd1eqwrdeq  13454  cshwidxmodr  13550  2swrd2eqwrdeq  13696  dvdsmultr1  15019  dvdssub2  15023  ndvdsadd  15134  mrcsscl  16280  latnle  17085  latabs1  17087  latabs2  17088  latj4rot  17102  grpsubf  17494  grpinvsub  17497  grpnpcan  17507  mulginvcom  17565  mulginvinv  17566  subgsubcl  17605  qussub  17654  ghmsub  17668  odhash3  17991  dvrcl  18686  unitdvcl  18687  abvsubtri  18835  lspsntrim  19098  lply1binomsc  19677  frlmsslss2  20114  lindsmm  20167  smadiadetglem2  20478  m2cpm  20546  m2cpminvid  20558  pmatcollpwscmat  20596  mp2pm2mp  20616  cpmidgsum  20673  cpmadugsumfi  20682  basgen2  20793  opnneiss  20922  restlp  20987  nmtri  22430  sincosq1lem  24249  logrec  24501  grpodivinv  27390  grpoinvdiv  27391  grpodivf  27392  nvmval2  27498  nvaddsub4  27512  nvpi  27522  nvmtri  27526  nvabs  27527  4ipval2  27563  ipval3  27564  isblo2  27638  blof  27640  nmblore  27641  nmlnoubi  27651  nmlnogt0  27652  shsubcl  28077  unopadj  28778  atexch  29240  atcvatlem  29244  ogrpsublt  29722  ind1  30079  inelsiga  30198  inelros  30236  mrsubcv  31407  mrsubvr  31408  nosupbnd1lem2  31855  btwnconn2  32209  ismtybnd  33606  lkrlsp2  34390  opcon2b  34484  opltcon2b  34493  oldmm3N  34506  oldmm4  34507  oldmj3  34510  oldmj4  34511  cmt2N  34537  cmt4N  34539  atleneN  34720  lplnri2N  34840  cdlema2N  35078  pmapojoinN  35254  ltrncnvatb  35424  trlval2  35450  trljat1  35453  cdleme18c  35580  cdleme19c  35593  cdlemeiota  35873  trlcocnv  36008  tendoplco2  36067  cdlemk6  36125  cdlemk7u  36158  cdlemk22  36181  cdlemk24-3  36191  cdlemkid2  36212  cdlemk11ta  36217  cdlemk11tc  36233  cdlemk47  36237  cdlemk52  36242  tendocnv  36310  dibelval1st1  36439  dibelval1st2N  36440  dihord2pre2  36515  mzprename  37312  pell14qrdivcl  37429  pwssplit4  37659  iocmbl  37798  relexpxpmin  38009  dvconstbi  38533  limsupgtlem  40009  dvbdfbdioolem1  40143  ibliccsinexp  40166  stoweidlem22  40239  fourierdlem42  40366  smfsuplem1  41017  pfxsuff1eqwrdeq  41407  pfxccatid  41430  divsub1dir  42307