Theorem 3syl 17

Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3syl.1	|- ( ph -> ps )
3syl.2	|- ( ps -> ch )
3syl.3	|- ( ch -> th )

Assertion

Ref	Expression
3syl	|- ( ph -> th )

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- ( ph -> ps )
2		3syl.2	. . 3 |- ( ps -> ch )
3	1, 2	syl 14	. 2 |- ( ph -> ch )
4		3syl.3	. 2 |- ( ch -> th )
5	3, 4	syl 14	1 |- ( ph -> th )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  4syl  18  simpl2im  386  hbim  1594  nfal  1625  19.9hd  1710  equsexd  1777  sbcof2  1858  aev  1860  sbequi  1887  nfsbd  2030  mo2n  2107  eupickb  2161  r19.29af2  2674  spc2gv  2898  spc3gv  2900  eqvincg  2931  sbcco3g  3186  ssrmof  3291  exmidsssnc  4299  exmid1stab  4304  snelpwi  4309  opth1  4334  frind  4455  onin  4489  abnexg  4549  reusv1  4561  xpexg  4846  reldmm  4956  dmexg  5002  rnexg  5003  elrelimasn  5109  relfld  5272  funimaexglem  5420  funimaexg  5421  fabexg  5532  fsnd  5637  elfvm  5681  nfvres  5684  funimass4  5705  elfvmptrab1  5750  funconstss  5774  f1oresrab  5820  resfunexg  5883  f1eqcocnv  5942  isores1  5965  isoini  5969  isose  5972  isopolem  5973  isosolem  5975  eusvobj2  6014  acexmidlemcase  6023  oprabid  6060  offval  6252  resfunexgALT  6279  offval3  6305  1stvalg  6314  2ndvalg  6315  1stcof  6335  2ndcof  6336  cnvf1o  6399  tposf12  6478  smores3  6502  smoiso  6511  tfr0dm  6531  tfrlemibxssdm  6536  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemssrecs  6548  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemssrecs  6561  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemres  6571  rdgss  6592  nnsucsssuc  6703  nntr2  6714  swoord1  6774  swoord2  6775  iinerm  6819  eroveu  6838  pmresg  6888  en1uniel  7021  dom1o  7045  pw2f1odclem  7063  fopwdom  7065  xpen  7074  ssenen  7080  isinfinf  7129  ac6sfi  7130  preimaf1ofi  7193  sbthlem1  7199  fczfsuppd  7222  fi0  7234  fiss  7236  supubti  7258  suplubti  7259  isotilem  7265  supisolem  7267  supisoex  7268  supisoti  7269  ordiso2  7294  eldju1st  7330  eldju2ndl  7331  updjud  7341  djudom  7352  ctmlemr  7367  enumctlemm  7373  nnnninfeq  7387  ctssexmid  7409  nninfwlpoimlemginf  7435  exmidonfinlem  7464  en2other2  7467  exmidaclem  7483  cc2lem  7545  cc3  7547  addclnq  7655  mulclnq  7656  1qec  7668  prarloclemarch2  7699  enq0tr  7714  addclnq0  7731  mulclnq0  7732  nq0m0r  7736  prarloclemlo  7774  prarloc  7783  genpml  7797  genpmu  7798  addnqprl  7809  addnqpru  7810  recnnpr  7828  prmuloc2  7847  1idpru  7871  ltexprlemm  7880  ltexprlemloc  7887  recexprlemm  7904  recexprlem1ssl  7913  caucvgprlemnkj  7946  caucvgprlemnbj  7947  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  caucvgprprlemk  7963  caucvgprprlemloccalc  7964  caucvgprprlemnkltj  7969  caucvgprprlemnjltk  7971  caucvgprprlemml  7974  caucvgprprlemmu  7975  caucvgprprlemlol  7978  caucvgprprlemexb  7987  caucvgprprlem1  7989  suplocexprlemml  7996  suplocexprlemlub  8004  addclsr  8033  mulclsr  8034  prsrcl  8064  caucvgsrlemoffcau  8078  peano5nnnn  8172  mulap0r  8854  nn1suc  9221  prime  9640  zindd  9659  xrlttri3  10093  xnn0xadd0  10163  fzopth  10358  fzsuc  10366  fzpred  10367  fzp1ss  10370  fztp  10375  fseq1p1m1  10391  1fv  10436  elfzom1elp1fzo  10510  ssfzo12  10532  fzosplitsn  10541  zsupcllemstep  10552  zsupcllemex  10553  infssuzledc  10557  divfl0  10619  fldiv4lem1div2uz2  10629  modqid  10674  modqmuladdim  10692  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  frecfzennn  10751  frecfzen2  10752  seq3val  10785  seqvalcd  10786  seqsplitg  10814  iseqf1olemqcl  10824  iseqf1olemnab  10826  iseqf1olemmo  10830  iseqf1olemqk  10832  seq3f1olemstep  10839  seqf1oglem2  10845  seq3id3  10849  seqhomog  10855  faclbnd  11066  faclbnd3  11068  bcm1k  11085  hashfz1  11108  hashfz  11148  hashfzp1  11151  fiubm  11155  hashfacen  11163  leisorel  11164  wrdexb  11191  wrdsymb  11207  wrdred1hash  11223  lsw0  11227  lswex  11231  ccat0  11239  ccatval2  11241  ccatw2s1leng  11281  ccats1val2  11283  swrds1  11315  swrdlsw  11316  ccats1pfxeqrex  11362  pfxccatin12lem1  11375  swrdccatin2  11376  swrdccat  11382  cats1fvd  11413  s1s2d  11441  s1s3d  11442  cjcj  11523  caucvgre  11621  r19.2uz  11633  resqrexlemgt0  11660  ltabs  11727  xrmaxiflemab  11887  xrmaxiflemlub  11888  nnf1o  12017  summodclem2a  12022  fsumf1o  12031  fisum0diag2  12088  modfsummodlemstep  12098  fsumparts  12111  clim2prod  12180  prodfap0  12186  prodmodclem2a  12217  fprodssdc  12231  fprodcllem  12247  ef0lem  12301  resinval  12356  recosval  12357  demoivreALT  12415  nn0o  12548  gcdmultiplez  12672  dvdssq  12682  nninfct  12692  eucalg  12711  lcmgcdnn  12734  dvdsnprmd  12777  prm2orodd  12778  isprm5lem  12793  qnumdenbi  12844  nn0gcdsq  12852  phibnd  12869  hashdvds  12873  phimullem  12877  prmdiveq  12888  hashgcdlem  12890  modprm0  12907  nnnn0modprm0  12908  modprmn0modprm0  12909  oddprm  12912  prm23lt5  12916  pcprendvds  12943  pcidlem  12976  pcmpt  12996  pcfac  13003  infpnlem2  13013  prmunb  13015  1arith  13020  4sqlem19  13062  unennn  13098  ennnfonelemk  13101  ennnfonelemjn  13103  ennnfonelemhf1o  13114  ennnfonelemex  13115  ennnfonelemf1  13119  ennnfonelemrn  13120  qnnen  13132  unbendc  13155  setsfun0  13198  srngbased  13310  srngplusgd  13311  srngmulrd  13312  srnginvld  13313  lmodbased  13328  lmodplusgd  13329  lmodscad  13330  lmodvscad  13331  ipsbased  13340  ipsaddgd  13341  ipsmulrd  13342  ipsscad  13343  ipsvscad  13344  ipsipd  13345  tgval  13425  prdsbas3  13450  isnsgrp  13569  ismnd  13582  dfgrp2e  13691  subgintm  13865  eqg0el  13896  ecqusaddcl  13906  kerf1ghm  13941  gsumfzconst  14008  imasrng  14050  srgisid  14080  srg1zr  14081  qusring2  14160  oppr1g  14176  dvdsr02  14200  isunitd  14201  crngunit  14206  unitpropdg  14243  elrhmunit  14272  subrngintm  14307  subrguss  14331  subrgunit  14334  subrgugrp  14335  subrgintm  14338  lmodfopnelem1  14420  rmodislmodlem  14446  rmodislmod  14447  lssuni  14459  islss3  14475  lss0v  14526  sraval  14533  rnglidlmmgm  14592  2idllidld  14602  2idlridld  14603  rng2idl0  14615  rng2idlsubg0  14618  zrh0  14721  znle  14733  zndvds0  14746  znf1o  14747  znleval  14749  znfi  14751  znhash  14752  znunit  14755  psrbaglecl  14771  psrbasg  14775  psradd  14780  psr0cl  14782  mpladd  14805  cldval  14910  ntrfval  14911  clsfval  14912  neifval  14951  neif  14952  neival  14954  cnclima  15034  cncnpi  15039  cnrest2  15047  cnrest2r  15048  cnptoprest  15050  cnpdis  15053  txvalex  15065  txval  15066  txcnmpt  15084  txdis  15088  cnmpt1t  15096  cnmpt2t  15104  hmeocnv  15118  hmeontr  15124  txhmeo  15130  xmetunirn  15169  xmettpos  15181  metn0  15189  xmetres  15193  metres  15194  blrnps  15222  blrn  15223  blin2  15243  blbas  15244  xmeterval  15246  xmettxlem  15320  xmettx  15321  metcnpi  15326  reldvg  15490  dvaddxx  15514  dvmulxx  15515  dviaddf  15516  dvimulf  15517  dvfre  15521  dvmptid  15527  dveflem  15537  elply2  15546  plyreres  15575  sinq12gt0  15641  rprelogbdiv  15768  logbgcd1irr  15778  fsumdvdsmul  15805  lgslem4  15822  lgsdirprm  15853  gausslemma2dlem0a  15868  gausslemma2dlem0f  15873  gausslemma2dlem0i  15876  gausslemma2dlem1a  15877  gausslemma2dlem1cl  15878  gausslemma2dlem5  15885  gausslemma2dlem6  15886  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisen  15893  lgsquadlem1  15896  m1lgs  15904  2lgslem1a  15907  2lgslem1c  15909  2lgsoddprmlem2  15925  edgval  16001  edgstruct  16005  umgrnloopv  16055  umgredgprv  16056  upgr1edc  16062  umgredgne  16091  usgredgssen  16103  umgr2edg1  16150  uspgredg2vlem  16161  uspgr1edc  16181  uhgrspansubgrlem  16217  wlkm  16280  wlkvtxiedg  16286  wlkvtxiedgg  16287  wlk1walkdom  16300  g0wlk0  16311  wlkres  16320  trlf1  16329  trlreslem  16330  trlres  16331  clwwlkg  16334  clwwlkccatlem  16341  clwwlknon  16370  eupthfi  16392  eupthseg  16393  eupthres  16398  trlsegvdeglem1  16401  trlsegvdeglem7  16407  trlsegvdegfi  16408  eupth2lem3lem2fi  16410  eupth2lem3lem3fi  16411  eupth2lem3lem6fi  16412  eupth2lem3lem4fi  16414  eupth2lem3lem7fi  16415  eupth2lem3fi  16417  eupth2lemsfi  16419  eupth2fi  16420  konigsbergssiedgwen  16427  bj-inex  16623  bj-sucexg  16638  bj-peano4  16671  setindis  16683  bdsetindis  16685  bj-inf2vnlem1  16686  nnsf  16731  nninfall  16735  nninfsellemeq  16740  sbthom  16754  gfsumval  16809