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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  4syl  18  simpl2im  390  hbim  1598  nfal  1629  19.9hd  1714  equsexd  1782  sbcof2  1863  aev  1865  sbequi  1892  nfsbd  2037  mo2n  2114  eupickb  2168  r19.29af2  2691  spc2gv  2916  spc3gv  2918  eqvincg  2950  sbcco3g  3205  ssrmof  3311  exmidsssnc  4340  exmid1stab  4345  snelpwi  4351  opth1  4376  frind  4497  onin  4531  abnexg  4592  reusv1  4604  xpexg  4889  reldmm  5000  dmexg  5046  rnexg  5047  elrelimasn  5153  relfld  5316  funimaexglem  5464  funimaexg  5465  fabexg  5579  fsnd  5684  elfvm  5729  nfvres  5732  funimass4  5753  elfvmptrab1  5801  funconstss  5827  f1oresrab  5873  resfunexg  5936  f1eqcocnv  5997  isores1  6020  isoini  6024  isose  6027  isopolem  6028  isosolem  6030  eusvobj2  6071  acexmidlemcase  6080  oprabid  6117  offval  6310  resfunexgALT  6337  offval3  6367  1stvalg  6376  2ndvalg  6377  1stcof  6397  2ndcof  6398  cnvf1o  6461  tposf12  6540  smores3  6564  smoiso  6573  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemssrecs  6610  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemssrecs  6623  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemres  6633  rdgss  6654  nnsucsssuc  6765  nntr2  6776  swoord1  6836  swoord2  6837  iinerm  6881  eroveu  6900  pmresg  6957  en1uniel  7091  dom1o  7116  pw2f1odclem  7134  fopwdom  7136  xpen  7145  mapunen  7151  ssenen  7152  isinfinf  7201  ac6sfi  7202  preimaf1ofi  7268  sbthlem1  7274  fczfsuppd  7297  fi0  7309  fiss  7311  supubti  7339  suplubti  7340  isotilem  7346  supisolem  7348  supisoex  7349  supisoti  7350  ordiso2  7375  eldju1st  7411  eldju2ndl  7412  updjud  7422  djudom  7433  ctmlemr  7448  enumctlemm  7454  nnnninfeq  7468  ctssexmid  7490  nninfwlpoimlemginf  7516  exmidonfinlem  7545  en2other2  7548  exmidaclem  7564  cc2lem  7632  cc3  7634  addclnq  7742  mulclnq  7743  1qec  7755  prarloclemarch2  7786  enq0tr  7801  addclnq0  7818  mulclnq0  7819  nq0m0r  7823  prarloclemlo  7861  prarloc  7870  genpml  7884  genpmu  7885  addnqprl  7896  addnqpru  7897  recnnpr  7915  prmuloc2  7934  1idpru  7958  ltexprlemm  7967  ltexprlemloc  7974  recexprlemm  7991  recexprlem1ssl  8000  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprprlemk  8050  caucvgprprlemloccalc  8051  caucvgprprlemnkltj  8056  caucvgprprlemnjltk  8058  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemlol  8065  caucvgprprlemexb  8074  caucvgprprlem1  8076  suplocexprlemml  8083  suplocexprlemlub  8091  addclsr  8120  mulclsr  8121  prsrcl  8151  caucvgsrlemoffcau  8165  peano5nnnn  8259  mulap0r  8945  indv  9297  nn1suc  9325  prime  9749  zindd  9768  xrlttri3  10209  xnn0xadd0  10279  fzopth  10477  fzsuc  10485  fzpred  10487  fzp1ss  10490  fztp  10495  fseq1p1m1  10511  1fv  10556  elfzom1elp1fzo  10630  ssfzo12  10652  fzosplitsn  10661  zsupcllemstep  10672  zsupcllemex  10673  infssuzledc  10677  divfl0  10744  fldiv4lem1div2uz2  10754  modqid  10799  modqmuladdim  10817  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  frecfzennn  10876  frecfzen2  10877  seq3val  10910  seqvalcd  10911  seqsplitg  10939  iseqf1olemqcl  10949  iseqf1olemnab  10951  iseqf1olemmo  10955  iseqf1olemqk  10957  seq3f1olemstep  10964  seqf1oglem2  10970  seq3id3  10974  seqhomog  10980  faclbnd  11193  faclbnd3  11195  bcm1k  11212  hashfz1  11236  hashfz  11276  hashfzp1  11279  fiubm  11285  hashfacen  11298  leisorel  11303  wrdexb  11330  wrdsymb  11346  wrdred1hash  11362  lsw0  11366  lswex  11370  ccat0  11378  ccatval2  11380  ccatw2s1leng  11420  ccats1val2  11422  swrds1  11454  swrdlsw  11455  ccats1pfxeqrex  11501  pfxccatin12lem1  11514  swrdccatin2  11515  swrdccat  11521  cats1fvd  11552  s1s2d  11580  s1s3d  11581  cjcj  11662  caucvgre  11761  r19.2uz  11773  resqrexlemgt0  11800  ltabs  11868  xrmaxiflemab  12029  xrmaxiflemlub  12030  nnf1o  12159  summodclem2a  12164  fsumf1o  12173  fisum0diag2  12230  modfsummodlemstep  12240  fsumparts  12253  clim2prod  12322  prodfap0  12328  prodmodclem2a  12359  fprodssdc  12373  fprodcllem  12389  ef0lem  12443  resinval  12498  recosval  12499  demoivreALT  12557  nn0o  12690  gcdmultiplez  12814  dvdssq  12824  nninfct  12834  eucalg  12853  lcmgcdnn  12876  dvdsnprmd  12919  prm2orodd  12920  isprm5lem  12936  qnumdenbi  12988  nn0gcdsq  12996  phibnd  13015  hashdvds  13019  phimullem  13023  prmdiveq  13034  hashgcdlem  13036  modprm0  13053  nnnn0modprm0  13054  modprmn0modprm0  13055  oddprm  13058  prm23lt5  13062  pcprendvds  13089  pcidlem  13122  pcmpt  13142  pcfac  13149  infpnlem2  13159  prmunb  13161  1arith  13166  4sqlem19  13208  ballotfilemfp1  13280  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemsima  13308  ballotfilemrv  13312  ballotfilemro  13315  ballotfilemfrc  13319  ballotfilemfrci  13320  ballotfilemfrceq  13321  ballotfilemfrcn0  13322  ballotfilemrinv0  13325  unennn  13337  ennnfonelemk  13340  ennnfonelemjn  13342  ennnfonelemhf1o  13353  ennnfonelemex  13354  ennnfonelemf1  13358  ennnfonelemrn  13359  qnnen  13371  unbendc  13394  setsfun0  13437  srngbased  13550  srngplusgd  13551  srngmulrd  13552  srnginvld  13553  lmodbased  13568  lmodplusgd  13569  lmodscad  13570  lmodvscad  13571  ipsbased  13580  ipsaddgd  13581  ipsmulrd  13582  ipsscad  13583  ipsvscad  13584  ipsipd  13585  tgval  13665  gzsumval2  13763  isnsgrp  13770  ismnd  13781  dfgrp2e  13882  subgintm  14050  eqg0el  14081  ecqusaddcl  14091  kerf1ghm  14126  gzsumconst  14192  gsumvalfi  14201  gsumf1ofi  14209  prdsbas3  14236  imasrng  14304  srgisid  14339  qusring2  14420  oppr1g  14437  dvdsr02  14461  isunitd  14462  crngunit  14467  unitpropdg  14504  elrhmunit  14533  subrngintm  14569  subrguss  14593  subrgunit  14596  subrgugrp  14597  subrgintm  14600  drngunz  14667  lmodfopnelem1  14710  rmodislmodlem  14736  rmodislmod  14737  lssuni  14749  islss3  14765  lss0v  14816  sraval  14823  rnglidlmmgm  14882  2idllidld  14892  2idlridld  14893  rng2idl0  14905  rng2idlsubg0  14908  zrh0  15009  znle  15021  zndvds0  15034  znf1o  15035  znleval  15037  znfi  15039  znhash  15040  znunit  15043  issubassa  15062  asclfval  15070  ascl0  15076  ascl1  15077  rnasclsubrg  15085  psrbaglecl  15109  psrbasg  15114  psradd  15119  psr0cl  15121  mpladd  15144  cldval  15249  ntrfval  15250  clsfval  15251  neifval  15290  neif  15291  neival  15293  cnclima  15373  cncnpi  15378  cnrest2  15386  cnrest2r  15387  cnptoprest  15389  cnpdis  15392  txvalex  15404  txval  15405  txcnmpt  15423  txdis  15427  cnmpt1t  15435  cnmpt2t  15443  hmeocnv  15457  hmeontr  15463  txhmeo  15469  xmetunirn  15508  xmettpos  15520  metn0  15528  xmetres  15532  metres  15533  blrnps  15561  blrn  15562  blin2  15582  blbas  15583  xmeterval  15585  xmettxlem  15659  xmettx  15660  metcnpi  15665  reldvg  15829  dvaddxx  15853  dvmulxx  15854  dviaddf  15855  dvimulf  15856  dvfre  15860  dvmptid  15866  dveflem  15876  elply2  15885  plyreres  15914  sinq12gt0  15981  logfac  16048  rprelogbdiv  16112  logbgcd1irr  16122  birthdaylem3  16146  ppinprm  16171  ppiqp1le  16173  fsumdvdsmul  16186  bcmono  16202  bposlem1  16209  bposlem3  16211  bposlem5  16213  lgslem4  16220  lgsdirprm  16251  gausslemma2dlem0a  16266  gausslemma2dlem0f  16271  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  gausslemma2dlem1cl  16276  gausslemma2dlem5  16283  gausslemma2dlem6  16284  gausslemma2d  16286  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisen  16291  lgsquadlem1  16294  m1lgs  16302  2lgslem1a  16305  2lgslem1c  16307  2lgsoddprmlem2  16323  edgval  16399  edgstruct  16403  umgrnloopv  16453  umgredgprv  16454  upgr1edc  16460  umgredgne  16489  usgredgssen  16501  umgr2edg1  16548  uspgredg2vlem  16559  uspgr1edc  16579  uhgrspansubgrlem  16615  wlkm  16678  wlkvtxiedg  16684  wlkvtxiedgg  16685  wlk1walkdom  16698  g0wlk0  16709  wlkres  16718  trlf1  16727  trlreslem  16728  trlres  16729  clwwlkg  16732  clwwlkccatlem  16739  clwwlknon  16768  eupthfi  16790  eupthseg  16791  eupthres  16796  trlsegvdeglem1  16799  trlsegvdeglem7  16805  trlsegvdegfi  16806  eupth2lem3lem2fi  16808  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  eupth2lem3fi  16815  eupth2lemsfi  16817  eupth2fi  16818  konigsbergssiedgwen  16825  bj-inex  17031  bj-sucexg  17046  bj-peano4  17079  setindis  17091  bdsetindis  17093  bj-inf2vnlem1  17094  wexmiddiffilem  17141  wexmiddifxy  17144  nnsf  17146  nninfall  17150  nninfsellemeq  17155  sbthom  17169