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  1863  stdpc5v  1938  19.37imv  1947  ax12w  2134  ax13dgen2  2139  ax12v  2179  spsd  2188  nf5r  2195  axc4  2320  equs5eALT  2366  ax13lem1  2373  nfeqf  2380  hbae  2430  ax12vALT  2468  2ax6elem  2469  sb1  2477  euimmo  2610  necon2ad  2941  necon4ad  2945  r19.37v  3161  spcimgfi1OLD  3517  rr19.28v  3637  moeq3  3686  reuimrmo  3719  sbeqalb  3819  csbexg  5268  ralxfrd  5366  ralxfrd2  5370  ralxfrALT  5373  copsexgw  5453  copsexg  5454  pwssun  5533  somo  5588  ssrel  5748  ssrelOLD  5749  relssres  5996  dmsnopg  6189  dfco2a  6222  dfpo2  6272  frpoinsg  6319  tz7.7  6361  ordunidif  6385  suctr  6423  trsucss  6425  suc11  6444  imadif  6603  dffv2  6959  fvmptd3f  6986  fvmptnf  6993  foco2  7084  fconst5  7183  fvf1pr  7285  isores3  7313  riotaxfrd  7381  ovmpt4g  7539  ovmpos  7540  ov2gf  7541  ovmpodf  7548  sorpsscmpl  7713  abnexg  7735  onint  7769  limuni3  7831  tfisg  7833  tfis  7834  tfinds  7839  limomss  7850  peano5  7872  fo2ndf  8103  frxp  8108  xpord2pred  8127  xpord2indlem  8129  soseq  8141  suppss2  8182  suppssfv  8184  rntpos  8221  fprlem1  8282  fprresex  8292  wfr3g  8301  onfununi  8313  smofvon2  8328  smo11  8336  smoord  8337  tfrlem11  8359  tz7.44-2  8378  tz7.48lem  8412  tz7.48-1  8414  tz7.49  8416  tz7.49c  8417  omordi  8533  omord  8535  omass  8547  oneo  8548  omeulem1  8549  omopth2  8551  oewordri  8559  oeworde  8560  nnmordi  8598  nnmord  8599  omabs  8618  nnneo  8622  omsmo  8625  naddcllem  8643  qsel  8772  eceqoveq  8798  domunsncan  9046  sucdom2OLD  9056  sbthlem1  9057  2pwuninel  9102  mapen  9111  infensuc  9125  rexdif1en  9128  findcard2  9134  pssnn  9138  ssfi  9143  sucdom2  9173  php  9177  onomeneq  9184  0sdom1dom  9192  sdom1  9196  dif1ennnALT  9229  ac6sfi  9238  frfi  9239  unblem1  9246  unblem2  9247  unbnn2  9251  nnsdomgOLD  9254  xpfiOLD  9277  domunfican  9279  fiintOLD  9285  fodomfir  9286  ixpfi2  9308  finsschain  9317  marypha1lem  9391  oiexg  9495  brwdom3  9542  inf3lem2  9589  inf3lem3  9590  cantnfval2  9629  cantnflt  9632  cantnflem1  9649  cnfcom  9660  ttrclss  9680  trcl  9688  epfrs  9691  frmin  9709  frinsg  9711  frr3g  9716  frrlem15  9717  r1sdom  9734  cardsdomel  9934  carduni  9941  pr2neOLD  9965  infpwfien  10022  carduniima  10056  dfac5  10089  dfac12r  10107  dfac12k  10108  kmlem11  10121  djuinf  10149  infxp  10174  cfsuc  10217  cfcoflem  10232  coftr  10233  infpssr  10268  fin23lem30  10302  isf32lem1  10313  isf34lem6  10340  fin1a2lem13  10372  fin1a2s  10374  axcc2lem  10396  domtriomlem  10402  axcclem  10417  ac6num  10439  zorn2lem5  10460  zorn2lem6  10461  axdclem2  10480  alephval2  10532  alephreg  10542  pwcfsdom  10543  axregndlem1  10562  axregnd  10564  axacndlem1  10567  axacndlem2  10568  axacndlem3  10569  axacndlem4  10570  axacnd  10572  gchi  10584  fpwwe2lem12  10602  canthp1  10614  gchpwdom  10630  wunfi  10681  tskwe2  10733  inar1  10735  gruen  10772  intgru  10774  indpi  10867  nqereu  10889  ltbtwnnq  10938  prnmadd  10957  genpcd  10966  prlem934  10993  ltexprlem1  10996  ltexprlem2  10997  ltexprlem7  11002  ltaprlem  11004  ltapr  11005  reclem4pr  11010  suplem2pr  11013  mulcmpblnr  11031  recexsrlem  11063  mulgt0sr  11065  supsrlem  11071  axpre-sup  11129  1re  11181  dedekindle  11345  addlsub  11601  recex  11817  nnunb  12445  0mnnnnn0  12481  prime  12622  zeo  12627  fnn0ind  12640  zindd  12642  btwnz  12644  lbzbi  12902  xrub  13279  elfznelfzo  13740  fvf1tp  13758  addmodlteq  13918  facwordi  14261  fiinfnf1o  14322  hashclb  14330  hashdom  14351  hashf1lem2  14428  seqcoll  14436  brfi1indALT  14482  ccatalpha  14565  pfxccatin12lem2a  14699  limsupbnd2  15456  rlimdm  15524  o1of2  15586  rlimno1  15627  isercoll  15641  caurcvg2  15651  caucvgb  15653  serf0  15654  zsum  15691  fsum2dlem  15743  fsum2d  15744  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fsumiun  15794  zprod  15910  fprod2dlem  15953  fprod2d  15954  odd2np1  16318  ndvdssub  16386  dfgcd2  16523  nprm  16665  maxprmfct  16686  rpexp  16699  pc2dvds  16857  pcfac  16877  unbenlem  16886  4sqlem12  16934  4sqlem17  16939  vdwlem13  16971  prmlem0  17083  mreiincl  17564  sscfn1  17786  initoid  17970  termoid  17971  funcestrcsetclem8  18115  funcsetcestrclem8  18130  pospo  18311  cnvpsb  18545  dirtr  18568  mulgaddcom  19037  mulginvcom  19038  gaass  19236  cntz2ss  19274  elsymgbas  19311  symgfix2  19353  pmtrfrn  19395  psgnran  19452  odmulg  19493  odhash3  19513  sylow2alem1  19554  sylow2alem2  19555  pj1eu  19633  efgs1b  19673  efgsfo  19676  efgredlemc  19682  efgredeu  19689  frgpuptinv  19708  lt6abl  19832  ghmcyg  19833  ablfac1eulem  20011  pgpfac1lem5  20018  ablsimpgfindlem1  20046  ringinvnz1ne0  20216  irredmul  20345  rnghmsscmap2  20545  rnghmsscmap  20546  rhmsscmap2  20574  rhmsscmap  20575  acsfn1p  20715  lspextmo  20970  lspsncv0  21063  pzriprnglem12  21409  psgnghm  21496  mplcoe1  21951  mplcoe5  21954  evlseu  21997  mhpsclcl  22041  mdetunilem7  22512  mdetunilem9  22514  chcoeffeq  22780  cnindis  23186  lmss  23192  lmcls  23196  lmcnp  23198  hausnei  23222  cmpsub  23294  tgcmp  23295  fiuncmp  23298  cmpfi  23302  bwth  23304  1stcrest  23347  2ndcdisj  23350  1stccnp  23356  comppfsc  23426  1stckgenlem  23447  txcls  23498  txcn  23520  txlm  23542  tx1stc  23544  xkococn  23554  hmphdis  23690  ptcmpfi  23707  isfild  23752  fgss2  23768  filconn  23777  trfil2  23781  ufileu  23813  filufint  23814  elfm2  23842  flftg  23890  fclssscls  23912  fclscf  23919  ufilcmp  23926  cnpfcf  23935  alexsubb  23940  alexsubALTlem4  23944  alexsubALT  23945  qustgpopn  24014  tsmsxp  24049  isust  24098  xmettri2  24235  blin2  24324  setsmstopn  24373  met2ndc  24418  metcnp3  24435  tngtopn  24545  reconnlem2  24723  xrge0tsms  24730  fsumcn  24768  bndth  24864  iscmet3lem2  25199  iscmet3  25200  ivthlem1  25359  ivthlem2  25360  ivthlem3  25361  ovolfiniun  25409  volfiniun  25455  ioombl1lem4  25469  ismbf3d  25562  mbfi1flimlem  25630  itg2seq  25650  itgfsum  25735  ellimc3  25787  dvmptfsum  25886  c1liplem1  25908  plypf1  26124  plydivex  26212  aannenlem1  26243  ulmval  26296  ulmcau  26311  ulmbdd  26314  ulmcn  26315  ulmdvlem3  26318  sineq0  26440  efopn  26574  cxpeq  26674  logbgcd1irr  26711  rlimcnp  26882  xrlimcnp  26885  lgsdir2lem2  27244  lgsne0  27253  2lgsoddprm  27334  2sqlem6  27341  2sqlem10  27346  2sqreunnltblem  27369  sltval2  27575  noetasuplem4  27655  conway  27718  madebdayim  27806  addsass  27919  onscutlt  28172  onsiso  28176  bdayn0p1  28265  zs12bday  28350  axcontlem2  28899  uhgr0vb  29006  uvtx01vtx  29331  uvtxupgrres  29342  fusgrn0degnn0  29434  finsumvtxdg2size  29485  cusgrm1rusgr  29517  wlkv0  29586  wlklenvclwlk  29590  uspgrn2crct  29745  frrusgrord  30277  numclwwlk1lem2fo  30294  isgrpo  30433  grpoidinvlem3  30442  vcdi  30501  vcdir  30502  vcass  30503  nvs  30599  nvtri  30606  blocnilem  30740  chintcli  31267  hsupss  31277  shlej1  31296  elspansn4  31509  spansncvi  31588  hoaddsub  31752  lnopl  31850  lnfnl  31867  riesz4i  31999  pjnormssi  32104  pj3si  32143  stlei  32176  stcltr2i  32211  dmdmd  32236  dmdbr5  32244  mdslmd1lem2  32262  atssma  32314  atcvatlem  32321  chirredlem1  32326  atcvat4i  32333  mdsymlem2  32340  mdsymlem6  32344  sumdmdlem2  32355  cdjreui  32368  elimifd  32479  disjxpin  32524  unifi3  32643  xrge0infss  32690  expgt0b  32748  xrge0tsmsd  33009  gsumle  33045  gsumvsca1  33186  gsumvsca2  33187  lmxrge0  33949  ismeas  34196  eulerpartlemb  34366  bnj849  34922  bnj1110  34979  srcmpltd  35077  swrdrevpfx  35111  cusgredgex2  35117  subgrwlk  35126  cusgr3cyclex  35130  umgr2cycllem  35134  umgr2cycl  35135  connpconn  35229  cvmseu  35270  cvmliftlem15  35292  cvmlift2lem1  35296  cvmlift2lem12  35308  satfv0fun  35365  satffunlem  35395  mclsind  35564  r1peuqusdeg1  35637  dfon2lem3  35780  dfon2lem4  35781  dfon2lem6  35783  dfon2lem8  35785  dfon2lem9  35786  hbntg  35800  cgrdegen  35999  funtransport  36026  ifscgr  36039  cgrxfr  36050  brofs2  36072  brifs2  36073  idinside  36079  btwnconn1lem7  36088  btwnconn1lem11  36092  btwnconn1lem12  36093  btwnconn1lem14  36095  broutsideof2  36117  btwnoutside  36120  outsideoftr  36124  in-ax8  36219  ss-ax8  36220  finminlem  36313  ntruni  36322  neibastop1  36354  ontgval  36426  ordtop  36431  ordcmp  36442  onint1  36444  bj-ax12w  36672  axc11n11r  36678  bj-ax12v3  36680  bj-nnfan  36743  bj-nnfand  36744  bj-nnflemea  36760  bj-19.42t  36768  bj-sbft  36770  bj-hbaeb2  36813  bj-spcimdv  36890  bj-spcimdvv  36891  bj-sngltag  36978  bj-xtagex  36984  bj-0int  37096  bj-ismooredr  37104  bj-inftyexpiinj  37204  nlpfvineqsn  37404  wl-ax13lem1  37489  wl-speqv  37517  wl-sbcom2d  37556  wl-ax11-lem3  37582  wl-ax11-lem8  37587  tan2h  37613  ptrest  37620  poimirlem20  37641  poimirlem22  37643  poimirlem26  37647  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  heicant  37656  voliunnfl  37665  volsupnfl  37666  itg2addnclem2  37673  itg2addnc  37675  itg2gt0cn  37676  ftc2nc  37703  filbcmb  37741  sdclem2  37743  seqpo  37748  nninfnub  37752  neificl  37754  prdstotbnd  37795  cnpwstotbnd  37798  heibor1lem  37810  heibor  37822  bfplem2  37824  opidonOLD  37853  exidu1  37857  grpokerinj  37894  rngoideu  37904  rngodi  37905  rngodir  37906  rngmgmbs4  37932  divrngidl  38029  prnc  38068  eqvrelqsel  38614  erimeq2  38677  prter2  38881  ax4fromc4  38894  hbae-o  38903  dvelimf-o  38929  ax12indn  38943  ax12inda2  38947  ax12a2-o  38950  l1cvpat  39054  atcvrj0  39429  pmaple  39762  paddasslem5  39825  pclfinN  39901  osumcllem11N  39967  pexmidlem8N  39978  dvheveccl  41113  dihord6apre  41257  lpolconN  41488  lcmineqlem1  42024  oexpreposd  42317  sn-it0e0  42411  cnreeu  42485  eu6w  42671  isnacs3  42705  pellexlem5  42828  pellex  42830  jm2.18  42984  jm2.15nn0  42999  jm2.16nn0  43000  dford3lem2  43023  ttac  43032  onexomgt  43237  onexoegt  43240  omabs2  43328  omcl3g  43330  tfsconcat0b  43342  naddgeoa  43390  safesnsupfiss  43411  rp-isfinite5  43513  cnvssb  43582  clcnvlem  43619  iunrelexpuztr  43715  rfovcnvf1od  44000  ntrrn  44118  nzss  44313  pm11.71  44393  axc11next  44402  hbntal  44550  eel2122old  44714  relwf  44964  modelaxreplem1  44975  ssclaxsep  44979  wfac8prim  44999  fsetsnf1  47057  2reu8i  47118  afvelima  47172  rlimdmafv  47182  rlimdmafv2  47263  elsprel  47480  sfprmdvdsmersenne  47608  perfectALTVlem2  47727  fpprwppr  47744  uhgrimedgi  47894  isuspgrim0lem  47897  uhgrimisgrgric  47935  gpgcubic  48074  gpg5nbgr3star  48076  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  copisnmnd  48161  funcringcsetcALTV2lem8  48289  funcringcsetclem8ALTV  48312  lindslinindsimp2lem5  48455  nn0sumshdig  48616  prelrrx2b  48707  itscnhlc0yqe  48752  iscnrm3lem2  48927  diag1f1lem  49299  spd  49671  setrec1lem4  49683  setrec2fun  49685  aacllem  49794