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  136  con3d  155  nsyli  160  syl5bi  243  syl5bir  244  syl5ib  245  adantld  491  adantrd  492  impel  506  mpan9  507  pm4.72  944  pm2.36  964  pm4.79  998  ecased  1028  ecase3ad  1029  alrimdh  1845  stdpc5v  1916  19.37imv  1925  ax12w  2104  ax13dgen2  2109  ax12v  2142  spsd  2150  nf5r  2157  nf5rOLD  2158  axc4  2303  equs5eALT  2342  ax13lem1  2346  nfeqf  2354  hbae  2410  ax12vALT  2449  2ax6elem  2450  euimmo  2668  necon2ad  2999  necon4ad  3003  r19.37v  3305  spcimgft  3529  rr19.28v  3600  moeq3  3639  reuimrmo  3670  sbeqalb  3764  csbexg  5105  ralxfrd  5200  ralxfrd2  5204  ralxfrALT  5207  copsexg  5273  pwssun  5344  somo  5398  ssrel  5543  relssres  5774  dmsnopg  5945  dfco2a  5974  wfisg  6058  tz7.7  6092  ordunidif  6114  suctr  6149  trsucss  6151  suc11  6169  imadif  6308  dffv2  6623  fvmptd3f  6649  fvmptnf  6656  foco2  6736  fconst5  6835  isores3  6951  riotaxfrd  7008  ovmpt4g  7153  ovmpos  7154  ov2gf  7155  ovmpodf  7162  sorpsscmpl  7318  abnexg  7335  onint  7366  limuni3  7423  tfis  7425  tfinds  7430  limomss  7441  peano5  7461  fo2ndf  7670  frxp  7673  suppss2  7715  suppssfv  7717  rntpos  7756  wfr3g  7804  wfrlem4OLD  7810  wfrlem5  7811  wfrlem17  7823  onfununi  7830  smofvon2  7845  smo11  7853  smoord  7854  tfrlem11  7876  tz7.44-2  7895  tz7.48lem  7928  tz7.48-1  7930  tz7.49  7932  tz7.49c  7933  omordi  8042  omord  8044  omass  8056  oneo  8057  omeulem1  8058  omopth2  8060  oewordri  8068  oeworde  8069  nnmordi  8107  nnmord  8108  omabs  8124  nnneo  8128  omsmo  8131  qsel  8226  eceqoveq  8252  domunsncan  8464  sbthlem1  8474  2pwuninel  8519  mapen  8528  infensuc  8542  sucdom2  8560  pssnn  8582  dif1en  8597  findcard2  8604  ac6sfi  8608  frfi  8609  unblem1  8616  unblem2  8617  unbnn2  8621  nnsdomg  8623  xpfi  8635  domunfican  8637  fiint  8641  ixpfi2  8668  finsschain  8677  marypha1lem  8743  oiexg  8845  brwdom3  8892  inf3lem2  8938  inf3lem3  8939  cantnfval2  8978  cantnflt  8981  cantnflem1  8998  cnfcom  9009  trcl  9016  epfrs  9019  r1sdom  9049  cardsdomel  9249  carduni  9256  pr2ne  9277  infpwfien  9334  carduniima  9368  dfac5  9400  dfac12r  9418  dfac12k  9419  kmlem11  9432  djuinf  9460  infxp  9483  cfsuc  9525  cfcoflem  9540  coftr  9541  infpssr  9576  fin23lem30  9610  isf32lem1  9621  isf34lem6  9648  fin1a2lem13  9680  fin1a2s  9682  axcc2lem  9704  domtriomlem  9710  axcclem  9725  ac6num  9747  zorn2lem5  9768  zorn2lem6  9769  axdclem2  9788  alephval2  9840  alephreg  9850  pwcfsdom  9851  axregndlem1  9870  axregnd  9872  axacndlem1  9875  axacndlem2  9876  axacndlem3  9877  axacndlem4  9878  axacnd  9880  gchi  9892  fpwwe2lem13  9910  canthp1  9922  gchpwdom  9938  wunfi  9989  tskwe2  10041  inar1  10043  gruen  10080  intgru  10082  indpi  10175  nqereu  10197  ltbtwnnq  10246  prnmadd  10265  genpcd  10274  prlem934  10301  ltexprlem1  10304  ltexprlem2  10305  ltexprlem7  10310  ltaprlem  10312  ltapr  10313  reclem4pr  10318  suplem2pr  10321  mulcmpblnr  10339  recexsrlem  10371  mulgt0sr  10373  supsrlem  10379  axpre-sup  10437  1re  10487  dedekindle  10651  addlsub  10904  recex  11120  nnunb  11741  0mnnnnn0  11777  prime  11912  zeo  11917  fnn0ind  11930  zindd  11932  btwnz  11933  lbzbi  12185  xrub  12555  elfznelfzo  12992  addmodlteq  13164  facwordi  13499  fiinfnf1o  13560  hashclb  13569  hashdom  13588  hashf1lem2  13662  seqcoll  13670  brfi1indALT  13704  ccatalpha  13791  pfxccatin12lem2a  13925  limsupbnd2  14674  rlimdm  14742  o1of2  14803  rlimno1  14844  isercoll  14858  caurcvg2  14868  caucvgb  14870  serf0  14871  zsum  14908  fsum2dlem  14958  fsum2d  14959  fsumabs  14989  fsumrlim  14999  fsumo1  15000  fsumiun  15009  zprod  15124  fprod2dlem  15167  fprod2d  15168  odd2np1  15523  ndvdssub  15593  dfgcd2  15723  nprm  15861  maxprmfct  15882  rpexp  15893  pc2dvds  16044  pcfac  16064  unbenlem  16073  4sqlem12  16121  4sqlem17  16126  vdwlem13  16158  prmlem0  16268  mreiincl  16696  sscfn1  16916  initoid  17094  termoid  17095  funcestrcsetclem8  17226  funcsetcestrclem8  17241  pospo  17412  cnvpsb  17652  dirtr  17675  mulgaddcom  18005  mulginvcom  18006  gaass  18168  cntz2ss  18204  elsymgbas  18241  symgfix2  18275  pmtrfrn  18317  psgnran  18374  odmulg  18413  odhash3  18431  sylow2alem1  18472  sylow2alem2  18473  pj1eu  18549  efgs1b  18589  efgsfo  18592  efgredlemc  18598  efgredeu  18605  frgpuptinv  18624  lt6abl  18736  ghmcyg  18737  ablfac1eulem  18911  pgpfac1lem5  18918  ringinvnz1ne0  19032  irredmul  19149  acsfn1p  19268  lspextmo  19518  lspsncv0  19608  mplcoe1  19933  mplcoe5  19936  evlseu  19983  psgnghm  20406  mdetunilem7  20911  mdetunilem9  20913  chcoeffeq  21178  cnindis  21584  lmss  21590  lmcls  21594  lmcnp  21596  hausnei  21620  cmpsub  21692  tgcmp  21693  fiuncmp  21696  cmpfi  21700  bwth  21702  1stcrest  21745  2ndcdisj  21748  1stccnp  21754  comppfsc  21824  1stckgenlem  21845  txcls  21896  txcn  21918  txlm  21940  tx1stc  21942  xkococn  21952  hmphdis  22088  ptcmpfi  22105  isfild  22150  fgss2  22166  filconn  22175  trfil2  22179  ufileu  22211  filufint  22212  elfm2  22240  flftg  22288  fclssscls  22310  fclscf  22317  ufilcmp  22324  cnpfcf  22333  alexsubb  22338  alexsubALTlem4  22342  alexsubALT  22343  qustgpopn  22411  tsmsxp  22446  isust  22495  xmettri2  22633  blin2  22722  setsmstopn  22771  met2ndc  22816  metcnp3  22833  tngtopn  22942  reconnlem2  23118  xrge0tsms  23125  fsumcn  23161  bndth  23245  iscmet3lem2  23578  iscmet3  23579  ivthlem1  23735  ivthlem2  23736  ivthlem3  23737  ovolfiniun  23785  volfiniun  23831  ioombl1lem4  23845  ismbf3d  23938  mbfi1flimlem  24006  itg2seq  24026  itgfsum  24110  ellimc3  24160  dvmptfsum  24255  c1liplem1  24276  plypf1  24485  plydivex  24569  aannenlem1  24600  ulmval  24651  ulmcau  24666  ulmbdd  24669  ulmcn  24670  ulmdvlem3  24673  sineq0  24792  efopn  24922  cxpeq  25019  logbgcd1irr  25053  rlimcnp  25225  xrlimcnp  25228  lgsdir2lem2  25584  lgsne0  25593  2lgsoddprm  25674  2sqlem6  25681  2sqlem10  25686  2sqreunnltblem  25709  axcontlem2  26434  uhgr0vb  26540  uvtx01vtx  26862  uvtxupgrres  26873  fusgrn0degnn0  26964  finsumvtxdg2size  27015  cusgrm1rusgr  27047  wlkv0  27115  uspgrn2crct  27273  frrusgrord  27812  numclwwlk1lem2fo  27829  isgrpo  27965  grpoidinvlem3  27974  vcdi  28033  vcdir  28034  vcass  28035  nvs  28131  nvtri  28138  blocnilem  28272  chintcli  28799  hsupss  28809  shlej1  28828  elspansn4  29041  spansncvi  29120  hoaddsub  29284  lnopl  29382  lnfnl  29399  riesz4i  29531  pjnormssi  29636  pj3si  29675  stlei  29708  stcltr2i  29743  dmdmd  29768  dmdbr5  29776  mdslmd1lem2  29794  atssma  29846  atcvatlem  29853  chirredlem1  29858  atcvat4i  29865  mdsymlem2  29872  mdsymlem6  29876  sumdmdlem2  29887  cdjreui  29900  elimifd  29987  disjxpin  30028  unifi3  30136  xrge0infss  30172  gsumle  30494  gsumvsca1  30497  gsumvsca2  30498  xrge0tsmsd  30503  lmxrge0  30812  ismeas  31075  eulerpartlemb  31243  bnj849  31813  bnj1110  31868  srcmpltd  31960  cusgredgex2  31981  subgrwlk  31987  cusgr3cyclex  31991  umgr2cycllem  31995  umgr2cycl  31996  connpconn  32090  cvmseu  32131  cvmliftlem15  32153  cvmlift2lem1  32157  cvmlift2lem12  32169  satfv0fun  32226  satffunlem  32256  mclsind  32425  dfpo2  32599  dfon2lem3  32638  dfon2lem4  32639  dfon2lem6  32641  dfon2lem8  32643  dfon2lem9  32644  hbntg  32659  tfisg  32664  dftrpred3g  32681  trpredrec  32686  frpoinsg  32690  frinsg  32696  soseq  32705  frr3g  32730  fprlem1  32746  frrlem15  32751  sltval2  32772  noetalem3  32828  conway  32873  cgrdegen  33074  funtransport  33101  ifscgr  33114  cgrxfr  33125  brofs2  33147  brifs2  33148  idinside  33154  btwnconn1lem7  33163  btwnconn1lem11  33167  btwnconn1lem12  33168  btwnconn1lem14  33170  broutsideof2  33192  btwnoutside  33195  outsideoftr  33199  finminlem  33275  ntruni  33284  neibastop1  33316  ontgval  33388  ordtop  33393  ordcmp  33404  onint1  33406  bj-ax12w  33609  axc11n11r  33616  bj-ax12v3  33618  bj-hbaeb2  33711  bj-spcimdv  33783  bj-spcimdvv  33784  bj-nnfant  33860  bj-nnfand  33861  bj-nnflemea  33876  bj-sbft  33879  bj-sngltag  33900  bj-xtagex  33906  bj-0int  33992  bj-ismooredr  34001  bj-inftyexpiinj  34049  nlpfvineqsn  34221  wl-ax13lem1  34277  wl-speqv  34295  wl-sbcom2d  34328  wl-ax11-lem3  34350  wl-ax11-lem8  34355  tan2h  34415  ptrest  34422  poimirlem20  34443  poimirlem22  34445  poimirlem26  34449  poimirlem30  34453  poimirlem31  34454  poimirlem32  34455  heicant  34458  voliunnfl  34467  volsupnfl  34468  itg2addnclem2  34475  itg2addnc  34477  itg2gt0cn  34478  ftc2nc  34507  filbcmb  34547  sdclem2  34549  seqpo  34554  nninfnub  34558  neificl  34560  prdstotbnd  34604  cnpwstotbnd  34607  heibor1lem  34619  heibor  34631  bfplem2  34633  opidonOLD  34662  exidu1  34666  grpokerinj  34703  rngoideu  34713  rngodi  34714  rngodir  34715  rngmgmbs4  34741  divrngidl  34838  prnc  34877  eqvrelqsel  35382  erim2  35442  prter2  35548  ax4fromc4  35561  hbae-o  35570  dvelimf-o  35596  ax12indn  35610  ax12inda2  35614  ax12a2-o  35617  l1cvpat  35721  atcvrj0  36095  pmaple  36428  paddasslem5  36491  pclfinN  36567  osumcllem11N  36633  pexmidlem8N  36644  dvheveccl  37779  dihord6apre  37923  lpolconN  38154  oexpreposd  38701  isnacs3  38792  pellexlem5  38915  pellex  38917  jm2.18  39070  jm2.15nn0  39085  jm2.16nn0  39086  dford3lem2  39109  ttac  39118  rp-isfinite5  39368  cnvssb  39431  clcnvlem  39468  iunrelexpuztr  39549  rfovcnvf1od  39835  ntrrn  39957  ablsimpgfindlem1  40165  nzss  40187  pm11.71  40267  axc11next  40276  hbntal  40426  eel2122old  40591  2reu8i  42828  afvelima  42882  rlimdmafv  42892  rlimdmafv2  42973  ichnfimlem1  43103  elsprel  43119  sfprmdvdsmersenne  43250  perfectALTVlem2  43369  fpprwppr  43386  copisnmnd  43558  rnghmsscmap2  43722  rnghmsscmap  43723  rhmsscmap2  43768  rhmsscmap  43769  funcringcsetcALTV2lem8  43792  funcringcsetclem8ALTV  43815  lindslinindsimp2lem5  43997  nn0sumshdig  44164  prelrrx2b  44182  itscnhlc0yqe  44227  spd  44261  setrec1lem4  44273  setrec2fun  44275  aacllem  44382