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  242  biimtrrid  243  imbitrid  244  adantld  490  adantrd  491  impel  505  mpan9  506  pm4.72  951  pm2.36  971  pm4.79  1005  ecased  1035  alrimdh  1864  stdpc5v  1939  19.37imv  1948  ax12w  2136  ax13dgen2  2141  ax12v  2181  spsd  2190  nf5r  2197  axc4  2322  equs5eALT  2367  ax13lem1  2374  nfeqf  2381  hbae  2431  ax12vALT  2469  2ax6elem  2470  sb1  2478  euimmo  2611  necon2ad  2943  necon4ad  2947  r19.37v  3158  spcimgfi1OLD  3503  rr19.28v  3623  moeq3  3671  reuimrmo  3704  sbeqalb  3804  csbexg  5248  ralxfrd  5346  ralxfrd2  5350  ralxfrALT  5353  copsexgw  5430  copsexg  5431  pwssun  5508  somo  5563  ssrel  5723  relssres  5971  dmsnopg  6160  dfco2a  6193  dfpo2  6243  frpoinsg  6290  tz7.7  6332  ordunidif  6356  suctr  6394  trsucss  6396  suc11  6415  imadif  6565  dffv2  6917  fvmptd3f  6944  fvmptnf  6951  foco2  7042  fconst5  7140  fvf1pr  7241  isores3  7269  riotaxfrd  7337  ovmpt4g  7493  ovmpos  7494  ov2gf  7495  ovmpodf  7502  sorpsscmpl  7667  abnexg  7689  onint  7723  limuni3  7782  tfisg  7784  tfis  7785  tfinds  7790  limomss  7801  peano5  7823  fo2ndf  8051  frxp  8056  xpord2pred  8075  xpord2indlem  8077  soseq  8089  suppss2  8130  suppssfv  8132  rntpos  8169  fprlem1  8230  fprresex  8240  wfr3g  8249  onfununi  8261  smofvon2  8276  smo11  8284  smoord  8285  tfrlem11  8307  tz7.44-2  8326  tz7.48lem  8360  tz7.48-1  8362  tz7.49  8364  tz7.49c  8365  omordi  8481  omord  8483  omass  8495  oneo  8496  omeulem1  8497  omopth2  8499  oewordri  8507  oeworde  8508  nnmordi  8546  nnmord  8547  omabs  8566  nnneo  8570  omsmo  8573  naddcllem  8591  qsel  8720  eceqoveq  8746  domunsncan  8990  sbthlem1  9000  2pwuninel  9045  mapen  9054  infensuc  9068  rexdif1en  9070  findcard2  9074  pssnn  9078  ssfi  9082  sucdom2  9112  php  9116  onomeneq  9123  0sdom1dom  9130  sdom1  9134  dif1ennnALT  9161  ac6sfi  9168  frfi  9169  unblem1  9176  unblem2  9177  unbnn2  9181  domunfican  9206  fodomfir  9212  ixpfi2  9234  finsschain  9243  marypha1lem  9317  oiexg  9421  brwdom3  9468  inf3lem2  9519  inf3lem3  9520  cantnfval2  9559  cantnflt  9562  cantnflem1  9579  cnfcom  9590  ttrclss  9610  trcl  9618  epfrs  9621  frmin  9639  frinsg  9641  frr3g  9646  frrlem15  9647  r1sdom  9664  cardsdomel  9864  carduni  9871  infpwfien  9950  carduniima  9984  dfac5  10017  dfac12r  10035  dfac12k  10036  kmlem11  10049  djuinf  10077  infxp  10102  cfsuc  10145  cfcoflem  10160  coftr  10161  infpssr  10196  fin23lem30  10230  isf32lem1  10241  isf34lem6  10268  fin1a2lem13  10300  fin1a2s  10302  axcc2lem  10324  domtriomlem  10330  axcclem  10345  ac6num  10367  zorn2lem5  10388  zorn2lem6  10389  axdclem2  10408  alephval2  10460  alephreg  10470  pwcfsdom  10471  axregndlem1  10490  axregnd  10492  axacndlem1  10495  axacndlem2  10496  axacndlem3  10497  axacndlem4  10498  axacnd  10500  gchi  10512  fpwwe2lem12  10530  canthp1  10542  gchpwdom  10558  wunfi  10609  tskwe2  10661  inar1  10663  gruen  10700  intgru  10702  indpi  10795  nqereu  10817  ltbtwnnq  10866  prnmadd  10885  genpcd  10894  prlem934  10921  ltexprlem1  10924  ltexprlem2  10925  ltexprlem7  10930  ltaprlem  10932  ltapr  10933  reclem4pr  10938  suplem2pr  10941  mulcmpblnr  10959  recexsrlem  10991  mulgt0sr  10993  supsrlem  10999  axpre-sup  11057  1re  11109  dedekindle  11274  addlsub  11530  recex  11746  nnunb  12374  0mnnnnn0  12410  prime  12551  zeo  12556  fnn0ind  12569  zindd  12571  btwnz  12573  lbzbi  12831  xrub  13208  elfznelfzo  13670  fvf1tp  13690  addmodlteq  13850  facwordi  14193  fiinfnf1o  14254  hashclb  14262  hashdom  14283  hashf1lem2  14360  seqcoll  14368  brfi1indALT  14414  ccatalpha  14498  pfxccatin12lem2a  14631  limsupbnd2  15387  rlimdm  15455  o1of2  15517  rlimno1  15558  isercoll  15572  caurcvg2  15582  caucvgb  15584  serf0  15585  zsum  15622  fsum2dlem  15674  fsum2d  15675  fsumabs  15705  fsumrlim  15715  fsumo1  15716  fsumiun  15725  zprod  15841  fprod2dlem  15884  fprod2d  15885  odd2np1  16249  ndvdssub  16317  dfgcd2  16454  nprm  16596  maxprmfct  16617  rpexp  16630  pc2dvds  16788  pcfac  16808  unbenlem  16817  4sqlem12  16865  4sqlem17  16870  vdwlem13  16902  prmlem0  17014  mreiincl  17495  sscfn1  17721  initoid  17905  termoid  17906  funcestrcsetclem8  18050  funcsetcestrclem8  18065  pospo  18246  cnvpsb  18482  dirtr  18505  mulgaddcom  19008  mulginvcom  19009  gaass  19207  cntz2ss  19245  elsymgbas  19284  symgfix2  19326  pmtrfrn  19368  psgnran  19425  odmulg  19466  odhash3  19486  sylow2alem1  19527  sylow2alem2  19528  pj1eu  19606  efgs1b  19646  efgsfo  19649  efgredlemc  19655  efgredeu  19662  frgpuptinv  19681  lt6abl  19805  ghmcyg  19806  ablfac1eulem  19984  pgpfac1lem5  19991  ablsimpgfindlem1  20019  gsumle  20055  ringinvnz1ne0  20216  irredmul  20345  rnghmsscmap2  20542  rnghmsscmap  20543  rhmsscmap2  20571  rhmsscmap  20572  acsfn1p  20712  lspextmo  20988  lspsncv0  21081  pzriprnglem12  21427  psgnghm  21515  mplcoe1  21970  mplcoe5  21973  evlseu  22016  mhpsclcl  22060  mdetunilem7  22531  mdetunilem9  22533  chcoeffeq  22799  cnindis  23205  lmss  23211  lmcls  23215  lmcnp  23217  hausnei  23241  cmpsub  23313  tgcmp  23314  fiuncmp  23317  cmpfi  23321  bwth  23323  1stcrest  23366  2ndcdisj  23369  1stccnp  23375  comppfsc  23445  1stckgenlem  23466  txcls  23517  txcn  23539  txlm  23561  tx1stc  23563  xkococn  23573  hmphdis  23709  ptcmpfi  23726  isfild  23771  fgss2  23787  filconn  23796  trfil2  23800  ufileu  23832  filufint  23833  elfm2  23861  flftg  23909  fclssscls  23931  fclscf  23938  ufilcmp  23945  cnpfcf  23954  alexsubb  23959  alexsubALTlem4  23963  alexsubALT  23964  qustgpopn  24033  tsmsxp  24068  isust  24117  xmettri2  24253  blin2  24342  setsmstopn  24391  met2ndc  24436  metcnp3  24453  tngtopn  24563  reconnlem2  24741  xrge0tsms  24748  fsumcn  24786  bndth  24882  iscmet3lem2  25217  iscmet3  25218  ivthlem1  25377  ivthlem2  25378  ivthlem3  25379  ovolfiniun  25427  volfiniun  25473  ioombl1lem4  25487  ismbf3d  25580  mbfi1flimlem  25648  itg2seq  25668  itgfsum  25753  ellimc3  25805  dvmptfsum  25904  c1liplem1  25926  plypf1  26142  plydivex  26230  aannenlem1  26261  ulmval  26314  ulmcau  26329  ulmbdd  26332  ulmcn  26333  ulmdvlem3  26336  sineq0  26458  efopn  26592  cxpeq  26692  logbgcd1irr  26729  rlimcnp  26900  xrlimcnp  26903  lgsdir2lem2  27262  lgsne0  27271  2lgsoddprm  27352  2sqlem6  27359  2sqlem10  27364  2sqreunnltblem  27387  sltval2  27593  noetasuplem4  27673  conway  27738  madebdayim  27831  addsass  27946  onscutlt  28199  onsiso  28203  bdayn0p1  28292  zs12zodd  28390  zs12bday  28392  axcontlem2  28941  uhgr0vb  29048  uvtx01vtx  29373  uvtxupgrres  29384  fusgrn0degnn0  29476  finsumvtxdg2size  29527  cusgrm1rusgr  29559  wlkv0  29626  wlklenvclwlk  29630  uspgrn2crct  29784  frrusgrord  30316  numclwwlk1lem2fo  30333  isgrpo  30472  grpoidinvlem3  30481  vcdi  30540  vcdir  30541  vcass  30542  nvs  30638  nvtri  30645  blocnilem  30779  chintcli  31306  hsupss  31316  shlej1  31335  elspansn4  31548  spansncvi  31627  hoaddsub  31791  lnopl  31889  lnfnl  31906  riesz4i  32038  pjnormssi  32143  pj3si  32182  stlei  32215  stcltr2i  32250  dmdmd  32275  dmdbr5  32283  mdslmd1lem2  32301  atssma  32353  atcvatlem  32360  chirredlem1  32365  atcvat4i  32372  mdsymlem2  32379  mdsymlem6  32383  sumdmdlem2  32394  cdjreui  32407  elimifd  32518  disjxpin  32563  unifi3  32689  xrge0infss  32738  expgt0b  32794  xrge0tsmsd  33037  gsumvsca1  33190  gsumvsca2  33191  lmxrge0  33960  ismeas  34207  eulerpartlemb  34376  bnj849  34932  bnj1110  34989  srcmpltd  35087  trssfir1omregs  35120  swrdrevpfx  35149  cusgredgex2  35155  subgrwlk  35164  cusgr3cyclex  35168  umgr2cycllem  35172  umgr2cycl  35173  connpconn  35267  cvmseu  35308  cvmliftlem15  35330  cvmlift2lem1  35334  cvmlift2lem12  35346  satfv0fun  35403  satffunlem  35433  mclsind  35602  r1peuqusdeg1  35675  dfon2lem3  35818  dfon2lem4  35819  dfon2lem6  35821  dfon2lem8  35823  dfon2lem9  35824  hbntg  35838  cgrdegen  36037  funtransport  36064  ifscgr  36077  cgrxfr  36088  brofs2  36110  brifs2  36111  idinside  36117  btwnconn1lem7  36126  btwnconn1lem11  36130  btwnconn1lem12  36131  btwnconn1lem14  36133  broutsideof2  36155  btwnoutside  36158  outsideoftr  36162  in-ax8  36257  ss-ax8  36258  finminlem  36351  ntruni  36360  neibastop1  36392  ontgval  36464  ordtop  36469  ordcmp  36480  onint1  36482  bj-ax12w  36710  axc11n11r  36716  bj-ax12v3  36718  bj-nnfan  36781  bj-nnfand  36782  bj-nnflemea  36798  bj-19.42t  36806  bj-sbft  36808  bj-hbaeb2  36851  bj-spcimdv  36928  bj-spcimdvv  36929  bj-sngltag  37016  bj-xtagex  37022  bj-0int  37134  bj-ismooredr  37142  bj-inftyexpiinj  37242  nlpfvineqsn  37442  wl-ax13lem1  37527  wl-speqv  37555  wl-sbcom2d  37594  wl-ax11-lem3  37620  wl-ax11-lem8  37625  tan2h  37651  ptrest  37658  poimirlem20  37679  poimirlem22  37681  poimirlem26  37685  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  heicant  37694  voliunnfl  37703  volsupnfl  37704  itg2addnclem2  37711  itg2addnc  37713  itg2gt0cn  37714  ftc2nc  37741  filbcmb  37779  sdclem2  37781  seqpo  37786  nninfnub  37790  neificl  37792  prdstotbnd  37833  cnpwstotbnd  37836  heibor1lem  37848  heibor  37860  bfplem2  37862  opidonOLD  37891  exidu1  37895  grpokerinj  37932  rngoideu  37942  rngodi  37943  rngodir  37944  rngmgmbs4  37970  divrngidl  38067  prnc  38106  eqvrelqsel  38652  erimeq2  38715  prter2  38919  ax4fromc4  38932  hbae-o  38941  dvelimf-o  38967  ax12indn  38981  ax12inda2  38985  ax12a2-o  38988  l1cvpat  39092  atcvrj0  39466  pmaple  39799  paddasslem5  39862  pclfinN  39938  osumcllem11N  40004  pexmidlem8N  40015  dvheveccl  41150  dihord6apre  41294  lpolconN  41525  lcmineqlem1  42061  oexpreposd  42354  sn-it0e0  42448  cnreeu  42522  eu6w  42708  isnacs3  42742  pellexlem5  42865  pellex  42867  jm2.18  43020  jm2.15nn0  43035  jm2.16nn0  43036  dford3lem2  43059  ttac  43068  onexomgt  43273  onexoegt  43276  omabs2  43364  omcl3g  43366  tfsconcat0b  43378  naddgeoa  43426  safesnsupfiss  43447  rp-isfinite5  43549  cnvssb  43618  clcnvlem  43655  iunrelexpuztr  43751  rfovcnvf1od  44036  ntrrn  44154  nzss  44349  pm11.71  44429  axc11next  44438  hbntal  44585  eel2122old  44749  relwf  44999  modelaxreplem1  45010  ssclaxsep  45014  wfac8prim  45034  fsetsnf1  47082  2reu8i  47143  afvelima  47197  rlimdmafv  47207  rlimdmafv2  47288  elsprel  47505  sfprmdvdsmersenne  47633  perfectALTVlem2  47752  fpprwppr  47769  uhgrimedgi  47920  isuspgrim0lem  47923  uhgrimisgrgric  47961  gpgcubic  48109  gpg5nbgr3star  48111  pgnioedg1  48138  pgnioedg2  48139  pgnioedg3  48140  pgnioedg4  48141  pgnioedg5  48142  copisnmnd  48199  funcringcsetcALTV2lem8  48327  funcringcsetclem8ALTV  48350  lindslinindsimp2lem5  48493  nn0sumshdig  48654  prelrrx2b  48745  itscnhlc0yqe  48790  iscnrm3lem2  48965  diag1f1lem  49337  spd  49709  setrec1lem4  49721  setrec2fun  49723  aacllem  49832