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  952  pm2.36  972  pm4.79  1006  ecased  1036  alrimdh  1865  stdpc5v  1940  19.37imv  1949  ax12w  2139  ax13dgen2  2144  ax12v  2186  spsd  2195  nf5r  2202  axc4  2327  equs5eALT  2372  ax13lem1  2379  nfeqf  2386  hbae  2436  ax12vALT  2474  2ax6elem  2475  sb1  2483  euimmo  2617  necon2ad  2948  necon4ad  2952  r19.37v  3163  spcimgfi1OLD  3506  rr19.28v  3623  moeq3  3671  reuimrmo  3704  sbeqalb  3804  csbexg  5256  ralxfrd  5354  ralxfrd2  5358  ralxfrALT  5361  copsexgw  5439  copsexg  5440  pwssun  5517  somo  5572  ssrel  5733  relssres  5982  dmsnopg  6172  dfco2a  6205  dfpo2  6255  frpoinsg  6302  tz7.7  6344  ordunidif  6368  suctr  6406  trsucss  6408  suc11  6427  imadif  6577  dffv2  6930  fvmptd3f  6958  fvmptnf  6965  foco2  7056  fconst5  7154  fvf1pr  7255  isores3  7283  riotaxfrd  7351  ovmpt4g  7507  ovmpos  7508  ov2gf  7509  ovmpodf  7516  sorpsscmpl  7681  abnexg  7703  onint  7737  limuni3  7796  tfisg  7798  tfis  7799  tfinds  7804  limomss  7815  peano5  7837  fo2ndf  8065  frxp  8070  xpord2pred  8089  xpord2indlem  8091  soseq  8103  suppss2  8144  suppssfv  8146  rntpos  8183  fprlem1  8244  fprresex  8254  wfr3g  8263  onfununi  8275  smofvon2  8290  smo11  8298  smoord  8299  tfrlem11  8321  tz7.44-2  8340  tz7.48lem  8374  tz7.48-1  8376  tz7.49  8378  tz7.49c  8379  omordi  8495  omord  8497  omass  8509  oneo  8510  omeulem1  8511  omopth2  8513  oewordri  8522  oeworde  8523  nnmordi  8561  nnmord  8562  omabs  8581  nnneo  8585  omsmo  8588  naddcllem  8606  qsel  8737  eceqoveq  8763  domunsncan  9009  sbthlem1  9019  2pwuninel  9064  mapen  9073  infensuc  9087  rexdif1en  9089  findcard2  9093  pssnn  9097  ssfi  9101  sucdom2  9131  php  9135  onomeneq  9142  0sdom1dom  9150  sdom1  9154  dif1ennnALT  9181  ac6sfi  9188  frfi  9189  unblem1  9196  unblem2  9197  unbnn2  9201  domunfican  9226  fodomfir  9232  ixpfi2  9254  finsschain  9263  unifi3  9266  marypha1lem  9340  oiexg  9444  brwdom3  9491  inf3lem2  9542  inf3lem3  9543  cantnfval2  9582  cantnflt  9585  cantnflem1  9602  cnfcom  9613  ttrclss  9633  trcl  9641  epfrs  9644  frmin  9665  frinsg  9667  frr3g  9672  frrlem15  9673  r1sdom  9690  cardsdomel  9890  carduni  9897  infpwfien  9976  carduniima  10010  dfac5  10043  dfac12r  10061  dfac12k  10062  kmlem11  10075  djuinf  10103  infxp  10128  cfsuc  10171  cfcoflem  10186  coftr  10187  infpssr  10222  fin23lem30  10256  isf32lem1  10267  isf34lem6  10294  fin1a2lem13  10326  fin1a2s  10328  axcc2lem  10350  domtriomlem  10356  axcclem  10371  ac6num  10393  zorn2lem5  10414  zorn2lem6  10415  axdclem2  10434  alephval2  10487  alephreg  10497  pwcfsdom  10498  axregndlem1  10517  axregnd  10519  axacndlem1  10522  axacndlem2  10523  axacndlem3  10524  axacndlem4  10525  axacnd  10527  gchi  10539  fpwwe2lem12  10557  canthp1  10569  gchpwdom  10585  wunfi  10636  tskwe2  10688  inar1  10690  gruen  10727  intgru  10729  indpi  10822  nqereu  10844  ltbtwnnq  10893  prnmadd  10912  genpcd  10921  prlem934  10948  ltexprlem1  10951  ltexprlem2  10952  ltexprlem7  10957  ltaprlem  10959  ltapr  10960  reclem4pr  10965  suplem2pr  10968  mulcmpblnr  10986  recexsrlem  11018  mulgt0sr  11020  supsrlem  11026  axpre-sup  11084  1re  11136  dedekindle  11301  addlsub  11557  recex  11773  nnunb  12401  0mnnnnn0  12437  prime  12577  zeo  12582  fnn0ind  12595  zindd  12597  btwnz  12599  lbzbi  12853  xrub  13231  elfznelfzo  13693  fvf1tp  13713  addmodlteq  13873  facwordi  14216  fiinfnf1o  14277  hashclb  14285  hashdom  14306  hashf1lem2  14383  seqcoll  14391  brfi1indALT  14437  ccatalpha  14521  pfxccatin12lem2a  14654  limsupbnd2  15410  rlimdm  15478  o1of2  15540  rlimno1  15581  isercoll  15595  caurcvg2  15605  caucvgb  15607  serf0  15608  zsum  15645  fsum2dlem  15697  fsum2d  15698  fsumabs  15728  fsumrlim  15738  fsumo1  15739  fsumiun  15748  zprod  15864  fprod2dlem  15907  fprod2d  15908  odd2np1  16272  ndvdssub  16340  dfgcd2  16477  nprm  16619  maxprmfct  16640  rpexp  16653  pc2dvds  16811  pcfac  16831  unbenlem  16840  4sqlem12  16888  4sqlem17  16893  vdwlem13  16925  prmlem0  17037  mreiincl  17519  sscfn1  17745  initoid  17929  termoid  17930  funcestrcsetclem8  18074  funcsetcestrclem8  18089  pospo  18270  cnvpsb  18506  dirtr  18529  mulgaddcom  19032  mulginvcom  19033  gaass  19230  cntz2ss  19268  elsymgbas  19307  symgfix2  19349  pmtrfrn  19391  psgnran  19448  odmulg  19489  odhash3  19509  sylow2alem1  19550  sylow2alem2  19551  pj1eu  19629  efgs1b  19669  efgsfo  19672  efgredlemc  19678  efgredeu  19685  frgpuptinv  19704  lt6abl  19828  ghmcyg  19829  ablfac1eulem  20007  pgpfac1lem5  20014  ablsimpgfindlem1  20042  gsumle  20078  ringinvnz1ne0  20239  irredmul  20369  rnghmsscmap2  20566  rnghmsscmap  20567  rhmsscmap2  20595  rhmsscmap  20596  acsfn1p  20736  lspextmo  21012  lspsncv0  21105  pzriprnglem12  21451  psgnghm  21539  mplcoe1  21996  mplcoe5  21999  evlseu  22042  mhpsclcl  22094  mdetunilem7  22566  mdetunilem9  22568  chcoeffeq  22834  cnindis  23240  lmss  23246  lmcls  23250  lmcnp  23252  hausnei  23276  cmpsub  23348  tgcmp  23349  fiuncmp  23352  cmpfi  23356  bwth  23358  1stcrest  23401  2ndcdisj  23404  1stccnp  23410  comppfsc  23480  1stckgenlem  23501  txcls  23552  txcn  23574  txlm  23596  tx1stc  23598  xkococn  23608  hmphdis  23744  ptcmpfi  23761  isfild  23806  fgss2  23822  filconn  23831  trfil2  23835  ufileu  23867  filufint  23868  elfm2  23896  flftg  23944  fclssscls  23966  fclscf  23973  ufilcmp  23980  cnpfcf  23989  alexsubb  23994  alexsubALTlem4  23998  alexsubALT  23999  qustgpopn  24068  tsmsxp  24103  isust  24152  xmettri2  24288  blin2  24377  setsmstopn  24426  met2ndc  24471  metcnp3  24488  tngtopn  24598  reconnlem2  24776  xrge0tsms  24783  fsumcn  24821  bndth  24917  iscmet3lem2  25252  iscmet3  25253  ivthlem1  25412  ivthlem2  25413  ivthlem3  25414  ovolfiniun  25462  volfiniun  25508  ioombl1lem4  25522  ismbf3d  25615  mbfi1flimlem  25683  itg2seq  25703  itgfsum  25788  ellimc3  25840  dvmptfsum  25939  c1liplem1  25961  plypf1  26177  plydivex  26265  aannenlem1  26296  ulmval  26349  ulmcau  26364  ulmbdd  26367  ulmcn  26368  ulmdvlem3  26371  sineq0  26493  efopn  26627  cxpeq  26727  logbgcd1irr  26764  rlimcnp  26935  xrlimcnp  26938  lgsdir2lem2  27297  lgsne0  27306  2lgsoddprm  27387  2sqlem6  27394  2sqlem10  27399  2sqreunnltblem  27422  sltval2  27628  noetasuplem4  27708  conway  27777  madebdayim  27870  addsass  27987  onscutlt  28245  onsiso  28252  addsonbday  28260  n0ssoldg  28333  bdayn0p1  28348  oldfib  28356  bdaypw2n0sbndlem  28442  bdayfinbndlem1  28446  zs12bdaylem1  28449  zs12zodd  28461  axcontlem2  29021  uhgr0vb  29128  uvtx01vtx  29453  uvtxupgrres  29464  fusgrn0degnn0  29556  finsumvtxdg2size  29607  cusgrm1rusgr  29639  wlkv0  29706  wlklenvclwlk  29710  uspgrn2crct  29864  frrusgrord  30399  numclwwlk1lem2fo  30416  isgrpo  30555  grpoidinvlem3  30564  vcdi  30623  vcdir  30624  vcass  30625  nvs  30721  nvtri  30728  blocnilem  30862  chintcli  31389  hsupss  31399  shlej1  31418  elspansn4  31631  spansncvi  31710  hoaddsub  31874  lnopl  31972  lnfnl  31989  riesz4i  32121  pjnormssi  32226  pj3si  32265  stlei  32298  stcltr2i  32333  dmdmd  32358  dmdbr5  32366  mdslmd1lem2  32384  atssma  32436  atcvatlem  32443  chirredlem1  32448  atcvat4i  32455  mdsymlem2  32462  mdsymlem6  32466  sumdmdlem2  32477  cdjreui  32490  elimifd  32600  disjxpin  32645  xrge0infss  32821  expgt0b  32878  xrge0tsmsd  33136  gsumvsca1  33289  gsumvsca2  33290  lmxrge0  34090  ismeas  34337  eulerpartlemb  34506  bnj849  35062  bnj1110  35119  srcmpltd  35217  trssfir1om  35248  fineqvinfep  35262  trssfir1omregs  35273  swrdrevpfx  35292  cusgredgex2  35298  subgrwlk  35307  cusgr3cyclex  35311  umgr2cycllem  35315  umgr2cycl  35316  connpconn  35410  cvmseu  35451  cvmliftlem15  35473  cvmlift2lem1  35477  cvmlift2lem12  35489  satfv0fun  35546  satffunlem  35576  mclsind  35745  r1peuqusdeg1  35818  dfon2lem3  35958  dfon2lem4  35959  dfon2lem6  35961  dfon2lem8  35963  dfon2lem9  35964  hbntg  35978  cgrdegen  36179  funtransport  36206  ifscgr  36219  cgrxfr  36230  brofs2  36252  brifs2  36253  idinside  36259  btwnconn1lem7  36268  btwnconn1lem11  36272  btwnconn1lem12  36273  btwnconn1lem14  36275  broutsideof2  36297  btwnoutside  36300  outsideoftr  36304  in-ax8  36399  ss-ax8  36400  finminlem  36493  ntruni  36502  neibastop1  36534  ontgval  36606  ordtop  36611  ordcmp  36622  onint1  36624  bj-ax12w  36853  axc11n11r  36859  bj-ax12v3  36861  bj-nnfan  36924  bj-nnfand  36925  bj-nnflemea  36941  bj-19.42t  36949  bj-sbft  36951  bj-hbaeb2  36994  bj-spcimdv  37071  bj-spcimdvv  37072  bj-sngltag  37159  bj-xtagex  37165  bj-0int  37277  bj-ismooredr  37285  bj-inftyexpiinj  37385  nlpfvineqsn  37585  wl-ax13lem1  37670  wl-speqv  37698  wl-sbcom2d  37737  tan2h  37784  ptrest  37791  poimirlem20  37812  poimirlem22  37814  poimirlem26  37818  poimirlem30  37822  poimirlem31  37823  poimirlem32  37824  heicant  37827  voliunnfl  37836  volsupnfl  37837  itg2addnclem2  37844  itg2addnc  37846  itg2gt0cn  37847  ftc2nc  37874  filbcmb  37912  sdclem2  37914  seqpo  37919  nninfnub  37923  neificl  37925  prdstotbnd  37966  cnpwstotbnd  37969  heibor1lem  37981  heibor  37993  bfplem2  37995  opidonOLD  38024  exidu1  38028  grpokerinj  38065  rngoideu  38075  rngodi  38076  rngodir  38077  rngmgmbs4  38103  divrngidl  38200  prnc  38239  rsp3eq  38539  eqvrelqsel  38872  erimeq2  38935  prter2  39178  ax4fromc4  39191  hbae-o  39200  dvelimf-o  39226  ax12indn  39240  ax12inda2  39244  ax12a2-o  39247  l1cvpat  39351  atcvrj0  39725  pmaple  40058  paddasslem5  40121  pclfinN  40197  osumcllem11N  40263  pexmidlem8N  40274  dvheveccl  41409  dihord6apre  41553  lpolconN  41784  lcmineqlem1  42320  oexpreposd  42613  sn-it0e0  42707  cnreeu  42781  eu6w  42955  isnacs3  42988  pellexlem5  43111  pellex  43113  jm2.18  43266  jm2.15nn0  43281  jm2.16nn0  43282  dford3lem2  43305  ttac  43314  onexomgt  43519  onexoegt  43522  omabs2  43610  omcl3g  43612  tfsconcat0b  43624  naddgeoa  43672  safesnsupfiss  43692  rp-isfinite5  43794  cnvssb  43863  clcnvlem  43900  iunrelexpuztr  43996  rfovcnvf1od  44281  ntrrn  44399  nzss  44594  pm11.71  44674  axc11next  44683  hbntal  44830  eel2122old  44994  relwf  45244  modelaxreplem1  45255  ssclaxsep  45259  wfac8prim  45279  fsetsnf1  47334  2reu8i  47395  afvelima  47449  rlimdmafv  47459  rlimdmafv2  47540  elsprel  47757  sfprmdvdsmersenne  47885  perfectALTVlem2  48004  fpprwppr  48021  uhgrimedgi  48172  isuspgrim0lem  48175  uhgrimisgrgric  48213  gpgcubic  48361  gpg5nbgr3star  48363  pgnioedg1  48390  pgnioedg2  48391  pgnioedg3  48392  pgnioedg4  48393  pgnioedg5  48394  copisnmnd  48451  funcringcsetcALTV2lem8  48579  funcringcsetclem8ALTV  48602  lindslinindsimp2lem5  48744  nn0sumshdig  48905  prelrrx2b  48996  itscnhlc0yqe  49041  iscnrm3lem2  49216  diag1f1lem  49587  spd  49959  setrec1lem4  49971  setrec2fun  49973  aacllem  50082