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  244  syl5bir  245  syl5ib  246  adantld  493  adantrd  494  impel  508  mpan9  509  pm4.72  946  pm2.36  966  pm4.79  1000  ecased  1030  ecase3ad  1031  alrimdh  1864  stdpc5v  1939  19.37imv  1948  ax12w  2137  ax13dgen2  2142  ax12v  2178  spsd  2186  nf5r  2193  nf5rOLD  2194  axc4  2340  equs5eALT  2385  ax13lem1  2392  nfeqf  2399  hbae  2453  ax12vALT  2492  2ax6elem  2493  sb1  2503  euimmo  2700  necon2ad  3031  necon4ad  3035  r19.37v  3344  spcimgft  3586  rr19.28v  3662  moeq3  3703  reuimrmo  3736  sbeqalb  3836  csbexg  5214  ralxfrd  5309  ralxfrd2  5313  ralxfrALT  5316  copsexgw  5381  copsexg  5382  pwssun  5456  somo  5510  ssrel  5657  relssres  5893  dmsnopg  6070  dfco2a  6099  wfisg  6183  tz7.7  6217  ordunidif  6239  suctr  6274  trsucss  6276  suc11  6294  imadif  6438  dffv2  6756  fvmptd3f  6783  fvmptnf  6790  foco2  6873  fconst5  6968  isores3  7088  riotaxfrd  7148  ovmpt4g  7297  ovmpos  7298  ov2gf  7299  ovmpodf  7306  sorpsscmpl  7460  abnexg  7478  onint  7510  limuni3  7567  tfis  7569  tfinds  7574  limomss  7585  peano5  7605  fo2ndf  7817  frxp  7820  suppss2  7864  suppssfv  7866  rntpos  7905  wfr3g  7953  wfrlem5  7959  wfrlem17  7971  onfununi  7978  smofvon2  7993  smo11  8001  smoord  8002  tfrlem11  8024  tz7.44-2  8043  tz7.48lem  8077  tz7.48-1  8079  tz7.49  8081  tz7.49c  8082  omordi  8192  omord  8194  omass  8206  oneo  8207  omeulem1  8208  omopth2  8210  oewordri  8218  oeworde  8219  nnmordi  8257  nnmord  8258  omabs  8274  nnneo  8278  omsmo  8281  qsel  8376  eceqoveq  8402  domunsncan  8617  sbthlem1  8627  2pwuninel  8672  mapen  8681  infensuc  8695  sucdom2  8714  pssnn  8736  dif1en  8751  findcard2  8758  ac6sfi  8762  frfi  8763  unblem1  8770  unblem2  8771  unbnn2  8775  nnsdomg  8777  xpfi  8789  domunfican  8791  fiint  8795  ixpfi2  8822  finsschain  8831  marypha1lem  8897  oiexg  8999  brwdom3  9046  inf3lem2  9092  inf3lem3  9093  cantnfval2  9132  cantnflt  9135  cantnflem1  9152  cnfcom  9163  trcl  9170  epfrs  9173  r1sdom  9203  cardsdomel  9403  carduni  9410  pr2ne  9431  infpwfien  9488  carduniima  9522  dfac5  9554  dfac12r  9572  dfac12k  9573  kmlem11  9586  djuinf  9614  infxp  9637  cfsuc  9679  cfcoflem  9694  coftr  9695  infpssr  9730  fin23lem30  9764  isf32lem1  9775  isf34lem6  9802  fin1a2lem13  9834  fin1a2s  9836  axcc2lem  9858  domtriomlem  9864  axcclem  9879  ac6num  9901  zorn2lem5  9922  zorn2lem6  9923  axdclem2  9942  alephval2  9994  alephreg  10004  pwcfsdom  10005  axregndlem1  10024  axregnd  10026  axacndlem1  10029  axacndlem2  10030  axacndlem3  10031  axacndlem4  10032  axacnd  10034  gchi  10046  fpwwe2lem13  10064  canthp1  10076  gchpwdom  10092  wunfi  10143  tskwe2  10195  inar1  10197  gruen  10234  intgru  10236  indpi  10329  nqereu  10351  ltbtwnnq  10400  prnmadd  10419  genpcd  10428  prlem934  10455  ltexprlem1  10458  ltexprlem2  10459  ltexprlem7  10464  ltaprlem  10466  ltapr  10467  reclem4pr  10472  suplem2pr  10475  mulcmpblnr  10493  recexsrlem  10525  mulgt0sr  10527  supsrlem  10533  axpre-sup  10591  1re  10641  dedekindle  10804  addlsub  11056  recex  11272  nnunb  11894  0mnnnnn0  11930  prime  12064  zeo  12069  fnn0ind  12082  zindd  12084  btwnz  12085  lbzbi  12337  xrub  12706  elfznelfzo  13143  addmodlteq  13315  facwordi  13650  fiinfnf1o  13711  hashclb  13720  hashdom  13741  hashf1lem2  13815  seqcoll  13823  brfi1indALT  13859  ccatalpha  13947  pfxccatin12lem2a  14089  limsupbnd2  14840  rlimdm  14908  o1of2  14969  rlimno1  15010  isercoll  15024  caurcvg2  15034  caucvgb  15036  serf0  15037  zsum  15075  fsum2dlem  15125  fsum2d  15126  fsumabs  15156  fsumrlim  15166  fsumo1  15167  fsumiun  15176  zprod  15291  fprod2dlem  15334  fprod2d  15335  odd2np1  15690  ndvdssub  15760  dfgcd2  15894  nprm  16032  maxprmfct  16053  rpexp  16064  pc2dvds  16215  pcfac  16235  unbenlem  16244  4sqlem12  16292  4sqlem17  16297  vdwlem13  16329  prmlem0  16439  mreiincl  16867  sscfn1  17087  initoid  17265  termoid  17266  funcestrcsetclem8  17397  funcsetcestrclem8  17412  pospo  17583  cnvpsb  17823  dirtr  17846  mulgaddcom  18251  mulginvcom  18252  gaass  18427  cntz2ss  18463  elsymgbas  18502  symgfix2  18544  pmtrfrn  18586  psgnran  18643  odmulg  18683  odhash3  18701  sylow2alem1  18742  sylow2alem2  18743  pj1eu  18822  efgs1b  18862  efgsfo  18865  efgredlemc  18871  efgredeu  18878  frgpuptinv  18897  lt6abl  19015  ghmcyg  19016  ablfac1eulem  19194  pgpfac1lem5  19201  ablsimpgfindlem1  19229  ringinvnz1ne0  19342  irredmul  19459  acsfn1p  19578  lspextmo  19828  lspsncv0  19918  mplcoe1  20246  mplcoe5  20249  evlseu  20296  psgnghm  20724  mdetunilem7  21227  mdetunilem9  21229  chcoeffeq  21494  cnindis  21900  lmss  21906  lmcls  21910  lmcnp  21912  hausnei  21936  cmpsub  22008  tgcmp  22009  fiuncmp  22012  cmpfi  22016  bwth  22018  1stcrest  22061  2ndcdisj  22064  1stccnp  22070  comppfsc  22140  1stckgenlem  22161  txcls  22212  txcn  22234  txlm  22256  tx1stc  22258  xkococn  22268  hmphdis  22404  ptcmpfi  22421  isfild  22466  fgss2  22482  filconn  22491  trfil2  22495  ufileu  22527  filufint  22528  elfm2  22556  flftg  22604  fclssscls  22626  fclscf  22633  ufilcmp  22640  cnpfcf  22649  alexsubb  22654  alexsubALTlem4  22658  alexsubALT  22659  qustgpopn  22728  tsmsxp  22763  isust  22812  xmettri2  22950  blin2  23039  setsmstopn  23088  met2ndc  23133  metcnp3  23150  tngtopn  23259  reconnlem2  23435  xrge0tsms  23442  fsumcn  23478  bndth  23562  iscmet3lem2  23895  iscmet3  23896  ivthlem1  24052  ivthlem2  24053  ivthlem3  24054  ovolfiniun  24102  volfiniun  24148  ioombl1lem4  24162  ismbf3d  24255  mbfi1flimlem  24323  itg2seq  24343  itgfsum  24427  ellimc3  24477  dvmptfsum  24572  c1liplem1  24593  plypf1  24802  plydivex  24886  aannenlem1  24917  ulmval  24968  ulmcau  24983  ulmbdd  24986  ulmcn  24987  ulmdvlem3  24990  sineq0  25109  efopn  25241  cxpeq  25338  logbgcd1irr  25372  rlimcnp  25543  xrlimcnp  25546  lgsdir2lem2  25902  lgsne0  25911  2lgsoddprm  25992  2sqlem6  25999  2sqlem10  26004  2sqreunnltblem  26027  axcontlem2  26751  uhgr0vb  26857  uvtx01vtx  27179  uvtxupgrres  27190  fusgrn0degnn0  27281  finsumvtxdg2size  27332  cusgrm1rusgr  27364  wlkv0  27432  wlklenvclwlk  27436  uspgrn2crct  27586  frrusgrord  28120  numclwwlk1lem2fo  28137  isgrpo  28274  grpoidinvlem3  28283  vcdi  28342  vcdir  28343  vcass  28344  nvs  28440  nvtri  28447  blocnilem  28581  chintcli  29108  hsupss  29118  shlej1  29137  elspansn4  29350  spansncvi  29429  hoaddsub  29593  lnopl  29691  lnfnl  29708  riesz4i  29840  pjnormssi  29945  pj3si  29984  stlei  30017  stcltr2i  30052  dmdmd  30077  dmdbr5  30085  mdslmd1lem2  30103  atssma  30155  atcvatlem  30162  chirredlem1  30167  atcvat4i  30174  mdsymlem2  30181  mdsymlem6  30185  sumdmdlem2  30196  cdjreui  30209  elimifd  30298  disjxpin  30338  unifi3  30448  xrge0infss  30484  xrge0tsmsd  30692  gsumle  30725  gsumvsca1  30854  gsumvsca2  30855  lmxrge0  31195  ismeas  31458  eulerpartlemb  31626  bnj849  32197  bnj1110  32254  srcmpltd  32346  swrdrevpfx  32363  cusgredgex2  32369  subgrwlk  32379  cusgr3cyclex  32383  umgr2cycllem  32387  umgr2cycl  32388  connpconn  32482  cvmseu  32523  cvmliftlem15  32545  cvmlift2lem1  32549  cvmlift2lem12  32561  satfv0fun  32618  satffunlem  32648  mclsind  32817  dfpo2  32991  dfon2lem3  33030  dfon2lem4  33031  dfon2lem6  33033  dfon2lem8  33035  dfon2lem9  33036  hbntg  33050  tfisg  33055  dftrpred3g  33072  trpredrec  33077  frpoinsg  33081  frinsg  33087  soseq  33096  frr3g  33121  fprlem1  33137  frrlem15  33142  sltval2  33163  noetalem3  33219  conway  33264  cgrdegen  33465  funtransport  33492  ifscgr  33505  cgrxfr  33516  brofs2  33538  brifs2  33539  idinside  33545  btwnconn1lem7  33554  btwnconn1lem11  33558  btwnconn1lem12  33559  btwnconn1lem14  33561  broutsideof2  33583  btwnoutside  33586  outsideoftr  33590  finminlem  33666  ntruni  33675  neibastop1  33707  ontgval  33779  ordtop  33784  ordcmp  33795  onint1  33797  bj-ax12w  34010  axc11n11r  34017  bj-ax12v3  34019  bj-nnfan  34077  bj-nnfand  34078  bj-nnflemea  34094  bj-19.42t  34102  bj-sbft  34104  bj-hbaeb2  34141  bj-spcimdv  34214  bj-spcimdvv  34215  bj-sngltag  34298  bj-xtagex  34304  bj-0int  34396  bj-ismooredr  34404  bj-inftyexpiinj  34494  nlpfvineqsn  34693  wl-ax13lem1  34761  wl-speqv  34777  wl-sbcom2d  34812  wl-ax11-lem3  34834  wl-ax11-lem8  34839  tan2h  34899  ptrest  34906  poimirlem20  34927  poimirlem22  34929  poimirlem26  34933  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  heicant  34942  voliunnfl  34951  volsupnfl  34952  itg2addnclem2  34959  itg2addnc  34961  itg2gt0cn  34962  ftc2nc  34991  filbcmb  35030  sdclem2  35032  seqpo  35037  nninfnub  35041  neificl  35043  prdstotbnd  35087  cnpwstotbnd  35090  heibor1lem  35102  heibor  35114  bfplem2  35116  opidonOLD  35145  exidu1  35149  grpokerinj  35186  rngoideu  35196  rngodi  35197  rngodir  35198  rngmgmbs4  35224  divrngidl  35321  prnc  35360  eqvrelqsel  35866  erim2  35926  prter2  36032  ax4fromc4  36045  hbae-o  36054  dvelimf-o  36080  ax12indn  36094  ax12inda2  36098  ax12a2-o  36101  l1cvpat  36205  atcvrj0  36579  pmaple  36912  paddasslem5  36975  pclfinN  37051  osumcllem11N  37117  pexmidlem8N  37128  dvheveccl  38263  dihord6apre  38407  lpolconN  38638  oexpreposd  39228  isnacs3  39356  pellexlem5  39479  pellex  39481  jm2.18  39634  jm2.15nn0  39649  jm2.16nn0  39650  dford3lem2  39673  ttac  39682  rp-isfinite5  39932  cnvssb  39995  clcnvlem  40032  iunrelexpuztr  40113  rfovcnvf1od  40399  ntrrn  40521  nzss  40698  pm11.71  40778  axc11next  40787  hbntal  40936  eel2122old  41101  2reu8i  43361  afvelima  43415  rlimdmafv  43425  rlimdmafv2  43506  ichnfimlem1  43670  elsprel  43686  sfprmdvdsmersenne  43817  perfectALTVlem2  43936  fpprwppr  43953  copisnmnd  44125  rnghmsscmap2  44293  rnghmsscmap  44294  rhmsscmap2  44339  rhmsscmap  44340  funcringcsetcALTV2lem8  44363  funcringcsetclem8ALTV  44386  lindslinindsimp2lem5  44566  nn0sumshdig  44732  prelrrx2b  44750  itscnhlc0yqe  44795  spd  44830  setrec1lem4  44842  setrec2fun  44844  aacllem  44951