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  2138  ax13dgen2  2143  ax12v  2183  spsd  2192  nf5r  2199  axc4  2324  equs5eALT  2369  ax13lem1  2376  nfeqf  2383  hbae  2433  ax12vALT  2471  2ax6elem  2472  sb1  2480  euimmo  2613  necon2ad  2944  necon4ad  2948  r19.37v  3159  spcimgfi1OLD  3502  rr19.28v  3619  moeq3  3667  reuimrmo  3700  sbeqalb  3800  csbexg  5250  ralxfrd  5348  ralxfrd2  5352  ralxfrALT  5355  copsexgw  5433  copsexg  5434  pwssun  5511  somo  5566  ssrel  5727  relssres  5975  dmsnopg  6165  dfco2a  6198  dfpo2  6248  frpoinsg  6295  tz7.7  6337  ordunidif  6361  suctr  6399  trsucss  6401  suc11  6420  imadif  6570  dffv2  6923  fvmptd3f  6950  fvmptnf  6957  foco2  7048  fconst5  7146  fvf1pr  7247  isores3  7275  riotaxfrd  7343  ovmpt4g  7499  ovmpos  7500  ov2gf  7501  ovmpodf  7508  sorpsscmpl  7673  abnexg  7695  onint  7729  limuni3  7788  tfisg  7790  tfis  7791  tfinds  7796  limomss  7807  peano5  7829  fo2ndf  8057  frxp  8062  xpord2pred  8081  xpord2indlem  8083  soseq  8095  suppss2  8136  suppssfv  8138  rntpos  8175  fprlem1  8236  fprresex  8246  wfr3g  8255  onfununi  8267  smofvon2  8282  smo11  8290  smoord  8291  tfrlem11  8313  tz7.44-2  8332  tz7.48lem  8366  tz7.48-1  8368  tz7.49  8370  tz7.49c  8371  omordi  8487  omord  8489  omass  8501  oneo  8502  omeulem1  8503  omopth2  8505  oewordri  8513  oeworde  8514  nnmordi  8552  nnmord  8553  omabs  8572  nnneo  8576  omsmo  8579  naddcllem  8597  qsel  8726  eceqoveq  8752  domunsncan  8997  sbthlem1  9007  2pwuninel  9052  mapen  9061  infensuc  9075  rexdif1en  9077  findcard2  9081  pssnn  9085  ssfi  9089  sucdom2  9119  php  9123  onomeneq  9130  0sdom1dom  9137  sdom1  9141  dif1ennnALT  9168  ac6sfi  9175  frfi  9176  unblem1  9183  unblem2  9184  unbnn2  9188  domunfican  9213  fodomfir  9219  ixpfi2  9241  finsschain  9250  marypha1lem  9324  oiexg  9428  brwdom3  9475  inf3lem2  9526  inf3lem3  9527  cantnfval2  9566  cantnflt  9569  cantnflem1  9586  cnfcom  9597  ttrclss  9617  trcl  9625  epfrs  9628  frmin  9649  frinsg  9651  frr3g  9656  frrlem15  9657  r1sdom  9674  cardsdomel  9874  carduni  9881  infpwfien  9960  carduniima  9994  dfac5  10027  dfac12r  10045  dfac12k  10046  kmlem11  10059  djuinf  10087  infxp  10112  cfsuc  10155  cfcoflem  10170  coftr  10171  infpssr  10206  fin23lem30  10240  isf32lem1  10251  isf34lem6  10278  fin1a2lem13  10310  fin1a2s  10312  axcc2lem  10334  domtriomlem  10340  axcclem  10355  ac6num  10377  zorn2lem5  10398  zorn2lem6  10399  axdclem2  10418  alephval2  10470  alephreg  10480  pwcfsdom  10481  axregndlem1  10500  axregnd  10502  axacndlem1  10505  axacndlem2  10506  axacndlem3  10507  axacndlem4  10508  axacnd  10510  gchi  10522  fpwwe2lem12  10540  canthp1  10552  gchpwdom  10568  wunfi  10619  tskwe2  10671  inar1  10673  gruen  10710  intgru  10712  indpi  10805  nqereu  10827  ltbtwnnq  10876  prnmadd  10895  genpcd  10904  prlem934  10931  ltexprlem1  10934  ltexprlem2  10935  ltexprlem7  10940  ltaprlem  10942  ltapr  10943  reclem4pr  10948  suplem2pr  10951  mulcmpblnr  10969  recexsrlem  11001  mulgt0sr  11003  supsrlem  11009  axpre-sup  11067  1re  11119  dedekindle  11284  addlsub  11540  recex  11756  nnunb  12384  0mnnnnn0  12420  prime  12560  zeo  12565  fnn0ind  12578  zindd  12580  btwnz  12582  lbzbi  12836  xrub  13213  elfznelfzo  13675  fvf1tp  13695  addmodlteq  13855  facwordi  14198  fiinfnf1o  14259  hashclb  14267  hashdom  14288  hashf1lem2  14365  seqcoll  14373  brfi1indALT  14419  ccatalpha  14503  pfxccatin12lem2a  14636  limsupbnd2  15392  rlimdm  15460  o1of2  15522  rlimno1  15563  isercoll  15577  caurcvg2  15587  caucvgb  15589  serf0  15590  zsum  15627  fsum2dlem  15679  fsum2d  15680  fsumabs  15710  fsumrlim  15720  fsumo1  15721  fsumiun  15730  zprod  15846  fprod2dlem  15889  fprod2d  15890  odd2np1  16254  ndvdssub  16322  dfgcd2  16459  nprm  16601  maxprmfct  16622  rpexp  16635  pc2dvds  16793  pcfac  16813  unbenlem  16822  4sqlem12  16870  4sqlem17  16875  vdwlem13  16907  prmlem0  17019  mreiincl  17500  sscfn1  17726  initoid  17910  termoid  17911  funcestrcsetclem8  18055  funcsetcestrclem8  18070  pospo  18251  cnvpsb  18487  dirtr  18510  mulgaddcom  19013  mulginvcom  19014  gaass  19211  cntz2ss  19249  elsymgbas  19288  symgfix2  19330  pmtrfrn  19372  psgnran  19429  odmulg  19470  odhash3  19490  sylow2alem1  19531  sylow2alem2  19532  pj1eu  19610  efgs1b  19650  efgsfo  19653  efgredlemc  19659  efgredeu  19666  frgpuptinv  19685  lt6abl  19809  ghmcyg  19810  ablfac1eulem  19988  pgpfac1lem5  19995  ablsimpgfindlem1  20023  gsumle  20059  ringinvnz1ne0  20220  irredmul  20349  rnghmsscmap2  20546  rnghmsscmap  20547  rhmsscmap2  20575  rhmsscmap  20576  acsfn1p  20716  lspextmo  20992  lspsncv0  21085  pzriprnglem12  21431  psgnghm  21519  mplcoe1  21973  mplcoe5  21976  evlseu  22019  mhpsclcl  22063  mdetunilem7  22534  mdetunilem9  22536  chcoeffeq  22802  cnindis  23208  lmss  23214  lmcls  23218  lmcnp  23220  hausnei  23244  cmpsub  23316  tgcmp  23317  fiuncmp  23320  cmpfi  23324  bwth  23326  1stcrest  23369  2ndcdisj  23372  1stccnp  23378  comppfsc  23448  1stckgenlem  23469  txcls  23520  txcn  23542  txlm  23564  tx1stc  23566  xkococn  23576  hmphdis  23712  ptcmpfi  23729  isfild  23774  fgss2  23790  filconn  23799  trfil2  23803  ufileu  23835  filufint  23836  elfm2  23864  flftg  23912  fclssscls  23934  fclscf  23941  ufilcmp  23948  cnpfcf  23957  alexsubb  23962  alexsubALTlem4  23966  alexsubALT  23967  qustgpopn  24036  tsmsxp  24071  isust  24120  xmettri2  24256  blin2  24345  setsmstopn  24394  met2ndc  24439  metcnp3  24456  tngtopn  24566  reconnlem2  24744  xrge0tsms  24751  fsumcn  24789  bndth  24885  iscmet3lem2  25220  iscmet3  25221  ivthlem1  25380  ivthlem2  25381  ivthlem3  25382  ovolfiniun  25430  volfiniun  25476  ioombl1lem4  25490  ismbf3d  25583  mbfi1flimlem  25651  itg2seq  25671  itgfsum  25756  ellimc3  25808  dvmptfsum  25907  c1liplem1  25929  plypf1  26145  plydivex  26233  aannenlem1  26264  ulmval  26317  ulmcau  26332  ulmbdd  26335  ulmcn  26336  ulmdvlem3  26339  sineq0  26461  efopn  26595  cxpeq  26695  logbgcd1irr  26732  rlimcnp  26903  xrlimcnp  26906  lgsdir2lem2  27265  lgsne0  27274  2lgsoddprm  27355  2sqlem6  27362  2sqlem10  27367  2sqreunnltblem  27390  sltval2  27596  noetasuplem4  27676  conway  27741  madebdayim  27834  addsass  27949  onscutlt  28202  onsiso  28206  bdayn0p1  28295  zs12zodd  28393  zs12bday  28395  axcontlem2  28945  uhgr0vb  29052  uvtx01vtx  29377  uvtxupgrres  29388  fusgrn0degnn0  29480  finsumvtxdg2size  29531  cusgrm1rusgr  29563  wlkv0  29630  wlklenvclwlk  29634  uspgrn2crct  29788  frrusgrord  30323  numclwwlk1lem2fo  30340  isgrpo  30479  grpoidinvlem3  30488  vcdi  30547  vcdir  30548  vcass  30549  nvs  30645  nvtri  30652  blocnilem  30786  chintcli  31313  hsupss  31323  shlej1  31342  elspansn4  31555  spansncvi  31634  hoaddsub  31798  lnopl  31896  lnfnl  31913  riesz4i  32045  pjnormssi  32150  pj3si  32189  stlei  32222  stcltr2i  32257  dmdmd  32282  dmdbr5  32290  mdslmd1lem2  32308  atssma  32360  atcvatlem  32367  chirredlem1  32372  atcvat4i  32379  mdsymlem2  32386  mdsymlem6  32390  sumdmdlem2  32401  cdjreui  32414  elimifd  32525  disjxpin  32570  unifi3  32698  xrge0infss  32747  expgt0b  32804  xrge0tsmsd  33049  gsumvsca1  33202  gsumvsca2  33203  lmxrge0  33986  ismeas  34233  eulerpartlemb  34402  bnj849  34958  bnj1110  35015  srcmpltd  35113  trssfir1om  35143  trssfir1omregs  35153  swrdrevpfx  35182  cusgredgex2  35188  subgrwlk  35197  cusgr3cyclex  35201  umgr2cycllem  35205  umgr2cycl  35206  connpconn  35300  cvmseu  35341  cvmliftlem15  35363  cvmlift2lem1  35367  cvmlift2lem12  35379  satfv0fun  35436  satffunlem  35466  mclsind  35635  r1peuqusdeg1  35708  dfon2lem3  35848  dfon2lem4  35849  dfon2lem6  35851  dfon2lem8  35853  dfon2lem9  35854  hbntg  35868  cgrdegen  36069  funtransport  36096  ifscgr  36109  cgrxfr  36120  brofs2  36142  brifs2  36143  idinside  36149  btwnconn1lem7  36158  btwnconn1lem11  36162  btwnconn1lem12  36163  btwnconn1lem14  36165  broutsideof2  36187  btwnoutside  36190  outsideoftr  36194  in-ax8  36289  ss-ax8  36290  finminlem  36383  ntruni  36392  neibastop1  36424  ontgval  36496  ordtop  36501  ordcmp  36512  onint1  36514  bj-ax12w  36742  axc11n11r  36748  bj-ax12v3  36750  bj-nnfan  36813  bj-nnfand  36814  bj-nnflemea  36830  bj-19.42t  36838  bj-sbft  36840  bj-hbaeb2  36883  bj-spcimdv  36960  bj-spcimdvv  36961  bj-sngltag  37048  bj-xtagex  37054  bj-0int  37166  bj-ismooredr  37174  bj-inftyexpiinj  37274  nlpfvineqsn  37474  wl-ax13lem1  37559  wl-speqv  37587  wl-sbcom2d  37626  tan2h  37673  ptrest  37680  poimirlem20  37701  poimirlem22  37703  poimirlem26  37707  poimirlem30  37711  poimirlem31  37712  poimirlem32  37713  heicant  37716  voliunnfl  37725  volsupnfl  37726  itg2addnclem2  37733  itg2addnc  37735  itg2gt0cn  37736  ftc2nc  37763  filbcmb  37801  sdclem2  37803  seqpo  37808  nninfnub  37812  neificl  37814  prdstotbnd  37855  cnpwstotbnd  37858  heibor1lem  37870  heibor  37882  bfplem2  37884  opidonOLD  37913  exidu1  37917  grpokerinj  37954  rngoideu  37964  rngodi  37965  rngodir  37966  rngmgmbs4  37992  divrngidl  38089  prnc  38128  eqvrelqsel  38733  erimeq2  38797  prter2  39001  ax4fromc4  39014  hbae-o  39023  dvelimf-o  39049  ax12indn  39063  ax12inda2  39067  ax12a2-o  39070  l1cvpat  39174  atcvrj0  39548  pmaple  39881  paddasslem5  39944  pclfinN  40020  osumcllem11N  40086  pexmidlem8N  40097  dvheveccl  41232  dihord6apre  41376  lpolconN  41607  lcmineqlem1  42143  oexpreposd  42441  sn-it0e0  42535  cnreeu  42609  eu6w  42795  isnacs3  42828  pellexlem5  42951  pellex  42953  jm2.18  43106  jm2.15nn0  43121  jm2.16nn0  43122  dford3lem2  43145  ttac  43154  onexomgt  43359  onexoegt  43362  omabs2  43450  omcl3g  43452  tfsconcat0b  43464  naddgeoa  43512  safesnsupfiss  43533  rp-isfinite5  43635  cnvssb  43704  clcnvlem  43741  iunrelexpuztr  43837  rfovcnvf1od  44122  ntrrn  44240  nzss  44435  pm11.71  44515  axc11next  44524  hbntal  44671  eel2122old  44835  relwf  45085  modelaxreplem1  45096  ssclaxsep  45100  wfac8prim  45120  fsetsnf1  47177  2reu8i  47238  afvelima  47292  rlimdmafv  47302  rlimdmafv2  47383  elsprel  47600  sfprmdvdsmersenne  47728  perfectALTVlem2  47847  fpprwppr  47864  uhgrimedgi  48015  isuspgrim0lem  48018  uhgrimisgrgric  48056  gpgcubic  48204  gpg5nbgr3star  48206  pgnioedg1  48233  pgnioedg2  48234  pgnioedg3  48235  pgnioedg4  48236  pgnioedg5  48237  copisnmnd  48294  funcringcsetcALTV2lem8  48422  funcringcsetclem8ALTV  48445  lindslinindsimp2lem5  48588  nn0sumshdig  48749  prelrrx2b  48840  itscnhlc0yqe  48885  iscnrm3lem2  49060  diag1f1lem  49432  spd  49804  setrec1lem4  49816  setrec2fun  49818  aacllem  49927