Theorem syl5 34

Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 25-May-2013.)

Hypotheses

Ref	Expression
syl5.1	⊢ (𝜑 → 𝜓)
syl5.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5

Step	Hyp	Ref	Expression
1		syl5.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl5.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5com 31	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4

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

This theorem is referenced by:  syl56  36  syl2im  40  imim12i  62  pm2.86d  108  con2d  134  con3d  152  nsyli  157  biimtrid  241  syl5bi  242  syl5bir  243  syl5ib  244  adantld  492  adantrd  493  impel  507  mpan9  508  pm4.72  948  pm2.36  968  pm4.79  1002  ecased  1033  ecase3adOLD  1035  alrimdh  1864  stdpc5v  1939  19.37imv  1949  ax12w  2127  ax13dgen2  2132  ax12v  2170  spsd  2178  nf5r  2185  axc4  2313  equs5eALT  2363  ax13lem1  2372  nfeqf  2379  hbae  2429  ax12vALT  2467  2ax6elem  2468  sb1  2477  euimmo  2616  necon2ad  2956  necon4ad  2960  r19.37v  3175  spcimgft  3531  rr19.28v  3604  moeq3  3652  reuimrmo  3685  sbeqalb  3789  csbexg  5243  ralxfrd  5340  ralxfrd2  5344  ralxfrALT  5347  copsexgw  5417  copsexg  5418  pwssun  5497  somo  5551  ssrel  5704  ssrelOLD  5705  relssres  5944  dmsnopg  6131  dfco2a  6164  dfpo2  6214  frpoinsg  6261  wfisgOLD  6272  tz7.7  6307  ordunidif  6329  suctr  6366  trsucss  6368  suc11  6386  imadif  6547  dffv2  6895  fvmptd3f  6922  fvmptnf  6929  foco2  7015  fconst5  7113  isores3  7238  riotaxfrd  7299  ovmpt4g  7452  ovmpos  7453  ov2gf  7454  ovmpodf  7461  sorpsscmpl  7619  abnexg  7638  onint  7672  limuni3  7731  tfis  7733  tfinds  7738  limomss  7749  peano5  7772  peano5OLD  7773  fo2ndf  7993  frxp  7998  suppss2  8047  suppssfv  8049  rntpos  8086  fprlem1  8147  fprresex  8157  wfr3g  8169  wfrlem5OLD  8175  wfrlem17OLD  8187  onfununi  8203  smofvon2  8218  smo11  8226  smoord  8227  tfrlem11  8250  tz7.44-2  8269  tz7.48lem  8303  tz7.48-1  8305  tz7.49  8307  tz7.49c  8308  omordi  8428  omord  8430  omass  8442  oneo  8443  omeulem1  8444  omopth2  8446  oewordri  8454  oeworde  8455  nnmordi  8493  nnmord  8494  omabs  8512  nnneo  8516  omsmo  8519  qsel  8616  eceqoveq  8642  domunsncan  8897  sucdom2OLD  8907  sbthlem1  8908  2pwuninel  8957  mapen  8966  infensuc  8980  findcard2  8985  pssnn  8989  ssfi  8994  sucdom2  9027  php  9031  onomeneq  9049  0sdom1dom  9059  sdom1  9063  pssnnOLD  9084  dif1enALT  9094  findcard2OLD  9100  ac6sfi  9102  frfi  9103  unblem1  9110  unblem2  9111  unbnn2  9115  nnsdomg  9117  xpfi  9129  domunfican  9131  fiint  9135  ixpfi2  9161  finsschain  9170  marypha1lem  9236  oiexg  9338  brwdom3  9385  inf3lem2  9431  inf3lem3  9432  cantnfval2  9471  cantnflt  9474  cantnflem1  9491  cnfcom  9502  ttrclss  9522  trcl  9530  epfrs  9533  frmin  9551  frinsg  9553  frr3g  9558  frrlem15  9559  r1sdom  9576  cardsdomel  9776  carduni  9783  pr2neOLD  9807  infpwfien  9864  carduniima  9898  dfac5  9930  dfac12r  9948  dfac12k  9949  kmlem11  9962  djuinf  9990  infxp  10017  cfsuc  10059  cfcoflem  10074  coftr  10075  infpssr  10110  fin23lem30  10144  isf32lem1  10155  isf34lem6  10182  fin1a2lem13  10214  fin1a2s  10216  axcc2lem  10238  domtriomlem  10244  axcclem  10259  ac6num  10281  zorn2lem5  10302  zorn2lem6  10303  axdclem2  10322  alephval2  10374  alephreg  10384  pwcfsdom  10385  axregndlem1  10404  axregnd  10406  axacndlem1  10409  axacndlem2  10410  axacndlem3  10411  axacndlem4  10412  axacnd  10414  gchi  10426  fpwwe2lem12  10444  canthp1  10456  gchpwdom  10472  wunfi  10523  tskwe2  10575  inar1  10577  gruen  10614  intgru  10616  indpi  10709  nqereu  10731  ltbtwnnq  10780  prnmadd  10799  genpcd  10808  prlem934  10835  ltexprlem1  10838  ltexprlem2  10839  ltexprlem7  10844  ltaprlem  10846  ltapr  10847  reclem4pr  10852  suplem2pr  10855  mulcmpblnr  10873  recexsrlem  10905  mulgt0sr  10907  supsrlem  10913  axpre-sup  10971  1re  11021  dedekindle  11185  addlsub  11437  recex  11653  nnunb  12275  0mnnnnn0  12311  prime  12447  zeo  12452  fnn0ind  12465  zindd  12467  btwnz  12469  lbzbi  12722  xrub  13092  elfznelfzo  13538  addmodlteq  13712  facwordi  14049  fiinfnf1o  14110  hashclb  14118  hashdom  14139  hashf1lem2  14215  seqcoll  14223  brfi1indALT  14259  ccatalpha  14343  pfxccatin12lem2a  14485  limsupbnd2  15237  rlimdm  15305  o1of2  15367  rlimno1  15410  isercoll  15424  caurcvg2  15434  caucvgb  15436  serf0  15437  zsum  15475  fsum2dlem  15527  fsum2d  15528  fsumabs  15558  fsumrlim  15568  fsumo1  15569  fsumiun  15578  zprod  15692  fprod2dlem  15735  fprod2d  15736  odd2np1  16095  ndvdssub  16163  dfgcd2  16299  nprm  16438  maxprmfct  16459  rpexp  16472  pc2dvds  16625  pcfac  16645  unbenlem  16654  4sqlem12  16702  4sqlem17  16707  vdwlem13  16739  prmlem0  16852  mreiincl  17350  sscfn1  17574  initoid  17761  termoid  17762  funcestrcsetclem8  17909  funcsetcestrclem8  17924  pospo  18108  cnvpsb  18342  dirtr  18365  mulgaddcom  18772  mulginvcom  18773  gaass  18948  cntz2ss  18984  elsymgbas  19026  symgfix2  19069  pmtrfrn  19111  psgnran  19168  odmulg  19208  odhash3  19226  sylow2alem1  19267  sylow2alem2  19268  pj1eu  19347  efgs1b  19387  efgsfo  19390  efgredlemc  19396  efgredeu  19403  frgpuptinv  19422  lt6abl  19541  ghmcyg  19542  ablfac1eulem  19720  pgpfac1lem5  19727  ablsimpgfindlem1  19755  ringinvnz1ne0  19876  irredmul  19996  acsfn1p  20112  lspextmo  20363  lspsncv0  20453  psgnghm  20830  mplcoe1  21283  mplcoe5  21286  evlseu  21338  mhpsclcl  21382  mdetunilem7  21812  mdetunilem9  21814  chcoeffeq  22080  cnindis  22488  lmss  22494  lmcls  22498  lmcnp  22500  hausnei  22524  cmpsub  22596  tgcmp  22597  fiuncmp  22600  cmpfi  22604  bwth  22606  1stcrest  22649  2ndcdisj  22652  1stccnp  22658  comppfsc  22728  1stckgenlem  22749  txcls  22800  txcn  22822  txlm  22844  tx1stc  22846  xkococn  22856  hmphdis  22992  ptcmpfi  23009  isfild  23054  fgss2  23070  filconn  23079  trfil2  23083  ufileu  23115  filufint  23116  elfm2  23144  flftg  23192  fclssscls  23214  fclscf  23221  ufilcmp  23228  cnpfcf  23237  alexsubb  23242  alexsubALTlem4  23246  alexsubALT  23247  qustgpopn  23316  tsmsxp  23351  isust  23400  xmettri2  23538  blin2  23627  setsmstopn  23678  met2ndc  23724  metcnp3  23741  tngtopn  23859  reconnlem2  24035  xrge0tsms  24042  fsumcn  24078  bndth  24166  iscmet3lem2  24501  iscmet3  24502  ivthlem1  24660  ivthlem2  24661  ivthlem3  24662  ovolfiniun  24710  volfiniun  24756  ioombl1lem4  24770  ismbf3d  24863  mbfi1flimlem  24932  itg2seq  24952  itgfsum  25036  ellimc3  25088  dvmptfsum  25184  c1liplem1  25205  plypf1  25418  plydivex  25502  aannenlem1  25533  ulmval  25584  ulmcau  25599  ulmbdd  25602  ulmcn  25603  ulmdvlem3  25606  sineq0  25725  efopn  25858  cxpeq  25955  logbgcd1irr  25989  rlimcnp  26160  xrlimcnp  26163  lgsdir2lem2  26519  lgsne0  26528  2lgsoddprm  26609  2sqlem6  26616  2sqlem10  26621  2sqreunnltblem  26644  axcontlem2  27378  uhgr0vb  27487  uvtx01vtx  27809  uvtxupgrres  27820  fusgrn0degnn0  27911  finsumvtxdg2size  27962  cusgrm1rusgr  27994  wlkv0  28063  wlklenvclwlk  28067  uspgrn2crct  28218  frrusgrord  28750  numclwwlk1lem2fo  28767  isgrpo  28904  grpoidinvlem3  28913  vcdi  28972  vcdir  28973  vcass  28974  nvs  29070  nvtri  29077  blocnilem  29211  chintcli  29738  hsupss  29748  shlej1  29767  elspansn4  29980  spansncvi  30059  hoaddsub  30223  lnopl  30321  lnfnl  30338  riesz4i  30470  pjnormssi  30575  pj3si  30614  stlei  30647  stcltr2i  30682  dmdmd  30707  dmdbr5  30715  mdslmd1lem2  30733  atssma  30785  atcvatlem  30792  chirredlem1  30797  atcvat4i  30804  mdsymlem2  30811  mdsymlem6  30815  sumdmdlem2  30826  cdjreui  30839  elimifd  30931  disjxpin  30972  unifi3  31092  xrge0infss  31128  xrge0tsmsd  31362  gsumle  31395  gsumvsca1  31524  gsumvsca2  31525  lmxrge0  31947  ismeas  32212  eulerpartlemb  32380  bnj849  32950  bnj1110  33007  srcmpltd  33099  swrdrevpfx  33123  cusgredgex2  33129  subgrwlk  33139  cusgr3cyclex  33143  umgr2cycllem  33147  umgr2cycl  33148  connpconn  33242  cvmseu  33283  cvmliftlem15  33305  cvmlift2lem1  33309  cvmlift2lem12  33321  satfv0fun  33378  satffunlem  33408  mclsind  33577  dfon2lem3  33806  dfon2lem4  33807  dfon2lem6  33809  dfon2lem8  33811  dfon2lem9  33812  hbntg  33826  tfisg  33831  xpord2pred  33837  xpord2ind  33839  xpord3ind  33845  soseq  33848  naddcllem  33876  sltval2  33904  noetasuplem4  33984  conway  34038  madebdayim  34115  cgrdegen  34351  funtransport  34378  ifscgr  34391  cgrxfr  34402  brofs2  34424  brifs2  34425  idinside  34431  btwnconn1lem7  34440  btwnconn1lem11  34444  btwnconn1lem12  34445  btwnconn1lem14  34447  broutsideof2  34469  btwnoutside  34472  outsideoftr  34476  finminlem  34552  ntruni  34561  neibastop1  34593  ontgval  34665  ordtop  34670  ordcmp  34681  onint1  34683  bj-ax12w  34903  axc11n11r  34910  bj-ax12v3  34912  bj-nnfan  34975  bj-nnfand  34976  bj-nnflemea  34992  bj-19.42t  35000  bj-sbft  35002  bj-hbaeb2  35045  bj-spcimdv  35124  bj-spcimdvv  35125  bj-sngltag  35217  bj-xtagex  35223  bj-0int  35316  bj-ismooredr  35324  bj-inftyexpiinj  35424  nlpfvineqsn  35624  wl-ax13lem1  35709  wl-speqv  35725  wl-sbcom2d  35760  wl-ax11-lem3  35782  wl-ax11-lem8  35787  tan2h  35813  ptrest  35820  poimirlem20  35841  poimirlem22  35843  poimirlem26  35847  poimirlem30  35851  poimirlem31  35852  poimirlem32  35853  heicant  35856  voliunnfl  35865  volsupnfl  35866  itg2addnclem2  35873  itg2addnc  35875  itg2gt0cn  35876  ftc2nc  35903  filbcmb  35942  sdclem2  35944  seqpo  35949  nninfnub  35953  neificl  35955  prdstotbnd  35996  cnpwstotbnd  35999  heibor1lem  36011  heibor  36023  bfplem2  36025  opidonOLD  36054  exidu1  36058  grpokerinj  36095  rngoideu  36105  rngodi  36106  rngodir  36107  rngmgmbs4  36133  divrngidl  36230  prnc  36269  eqvrelqsel  36771  erim2  36831  prter2  36937  ax4fromc4  36950  hbae-o  36959  dvelimf-o  36985  ax12indn  36999  ax12inda2  37003  ax12a2-o  37006  l1cvpat  37110  atcvrj0  37484  pmaple  37817  paddasslem5  37880  pclfinN  37956  osumcllem11N  38022  pexmidlem8N  38033  dvheveccl  39168  dihord6apre  39312  lpolconN  39543  lcmineqlem1  40079  oexpreposd  40358  sn-it0e0  40434  cnreeu  40475  isnacs3  40569  pellexlem5  40692  pellex  40694  jm2.18  40848  jm2.15nn0  40863  jm2.16nn0  40864  dford3lem2  40887  ttac  40896  rp-isfinite5  41162  cnvssb  41232  clcnvlem  41269  iunrelexpuztr  41365  rfovcnvf1od  41650  ntrrn  41770  nzss  41973  pm11.71  42053  axc11next  42062  hbntal  42211  eel2122old  42376  fsetsnf1  44604  2reu8i  44663  afvelima  44717  rlimdmafv  44727  rlimdmafv2  44808  elsprel  44985  sfprmdvdsmersenne  45113  perfectALTVlem2  45232  fpprwppr  45249  copisnmnd  45421  rnghmsscmap2  45589  rnghmsscmap  45590  rhmsscmap2  45635  rhmsscmap  45636  funcringcsetcALTV2lem8  45659  funcringcsetclem8ALTV  45682  lindslinindsimp2lem5  45861  nn0sumshdig  46027  prelrrx2b  46118  itscnhlc0yqe  46163  iscnrm3lem2  46286  spd  46442  setrec1lem4  46454  setrec2fun  46456  aacllem  46563