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  3164  spcimgfi1OLD  3507  rr19.28v  3624  moeq3  3672  reuimrmo  3705  sbeqalb  3805  csbexg  5257  ralxfrd  5355  ralxfrd2  5359  ralxfrALT  5362  copsexgw  5446  copsexg  5447  pwssun  5524  somo  5579  ssrel  5740  relssres  5989  dmsnopg  6179  dfco2a  6212  dfpo2  6262  frpoinsg  6309  tz7.7  6351  ordunidif  6375  suctr  6413  trsucss  6415  suc11  6434  imadif  6584  dffv2  6937  fvmptd3f  6965  fvmptnf  6972  foco2  7063  fconst5  7162  fvf1pr  7263  isores3  7291  riotaxfrd  7359  ovmpt4g  7515  ovmpos  7516  ov2gf  7517  ovmpodf  7524  sorpsscmpl  7689  abnexg  7711  onint  7745  limuni3  7804  tfisg  7806  tfis  7807  tfinds  7812  limomss  7823  peano5  7845  fo2ndf  8073  frxp  8078  xpord2pred  8097  xpord2indlem  8099  soseq  8111  suppss2  8152  suppssfv  8154  rntpos  8191  fprlem1  8252  fprresex  8262  wfr3g  8271  onfununi  8283  smofvon2  8298  smo11  8306  smoord  8307  tfrlem11  8329  tz7.44-2  8348  tz7.48lem  8382  tz7.48-1  8384  tz7.49  8386  tz7.49c  8387  omordi  8503  omord  8505  omass  8517  oneo  8518  omeulem1  8519  omopth2  8521  oewordri  8530  oeworde  8531  nnmordi  8569  nnmord  8570  omabs  8589  nnneo  8593  omsmo  8596  naddcllem  8614  qsel  8745  eceqoveq  8771  domunsncan  9017  sbthlem1  9027  2pwuninel  9072  mapen  9081  infensuc  9095  rexdif1en  9097  findcard2  9101  pssnn  9105  ssfi  9109  sucdom2  9139  php  9143  onomeneq  9150  0sdom1dom  9158  sdom1  9162  dif1ennnALT  9189  ac6sfi  9196  frfi  9197  unblem1  9204  unblem2  9205  unbnn2  9209  domunfican  9234  fodomfir  9240  ixpfi2  9262  finsschain  9271  unifi3  9274  marypha1lem  9348  oiexg  9452  brwdom3  9499  inf3lem2  9550  inf3lem3  9551  cantnfval2  9590  cantnflt  9593  cantnflem1  9610  cnfcom  9621  ttrclss  9641  trcl  9649  epfrs  9652  frmin  9673  frinsg  9675  frr3g  9680  frrlem15  9681  r1sdom  9698  cardsdomel  9898  carduni  9905  infpwfien  9984  carduniima  10018  dfac5  10051  dfac12r  10069  dfac12k  10070  kmlem11  10083  djuinf  10111  infxp  10136  cfsuc  10179  cfcoflem  10194  coftr  10195  infpssr  10230  fin23lem30  10264  isf32lem1  10275  isf34lem6  10302  fin1a2lem13  10334  fin1a2s  10336  axcc2lem  10358  domtriomlem  10364  axcclem  10379  ac6num  10401  zorn2lem5  10422  zorn2lem6  10423  axdclem2  10442  alephval2  10495  alephreg  10505  pwcfsdom  10506  axregndlem1  10525  axregnd  10527  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacnd  10535  gchi  10547  fpwwe2lem12  10565  canthp1  10577  gchpwdom  10593  wunfi  10644  tskwe2  10696  inar1  10698  gruen  10735  intgru  10737  indpi  10830  nqereu  10852  ltbtwnnq  10901  prnmadd  10920  genpcd  10929  prlem934  10956  ltexprlem1  10959  ltexprlem2  10960  ltexprlem7  10965  ltaprlem  10967  ltapr  10968  reclem4pr  10973  suplem2pr  10976  mulcmpblnr  10994  recexsrlem  11026  mulgt0sr  11028  supsrlem  11034  axpre-sup  11092  1re  11144  dedekindle  11309  addlsub  11565  recex  11781  nnunb  12409  0mnnnnn0  12445  prime  12585  zeo  12590  fnn0ind  12603  zindd  12605  btwnz  12607  lbzbi  12861  xrub  13239  elfznelfzo  13701  fvf1tp  13721  addmodlteq  13881  facwordi  14224  fiinfnf1o  14285  hashclb  14293  hashdom  14314  hashf1lem2  14391  seqcoll  14399  brfi1indALT  14445  ccatalpha  14529  pfxccatin12lem2a  14662  limsupbnd2  15418  rlimdm  15486  o1of2  15548  rlimno1  15589  isercoll  15603  caurcvg2  15613  caucvgb  15615  serf0  15616  zsum  15653  fsum2dlem  15705  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  zprod  15872  fprod2dlem  15915  fprod2d  15916  odd2np1  16280  ndvdssub  16348  dfgcd2  16485  nprm  16627  maxprmfct  16648  rpexp  16661  pc2dvds  16819  pcfac  16839  unbenlem  16848  4sqlem12  16896  4sqlem17  16901  vdwlem13  16933  prmlem0  17045  mreiincl  17527  sscfn1  17753  initoid  17937  termoid  17938  funcestrcsetclem8  18082  funcsetcestrclem8  18097  pospo  18278  cnvpsb  18514  dirtr  18537  mulgaddcom  19040  mulginvcom  19041  gaass  19238  cntz2ss  19276  elsymgbas  19315  symgfix2  19357  pmtrfrn  19399  psgnran  19456  odmulg  19497  odhash3  19517  sylow2alem1  19558  sylow2alem2  19559  pj1eu  19637  efgs1b  19677  efgsfo  19680  efgredlemc  19686  efgredeu  19693  frgpuptinv  19712  lt6abl  19836  ghmcyg  19837  ablfac1eulem  20015  pgpfac1lem5  20022  ablsimpgfindlem1  20050  gsumle  20086  ringinvnz1ne0  20247  irredmul  20377  rnghmsscmap2  20574  rnghmsscmap  20575  rhmsscmap2  20603  rhmsscmap  20604  acsfn1p  20744  lspextmo  21020  lspsncv0  21113  pzriprnglem12  21459  psgnghm  21547  mplcoe1  22004  mplcoe5  22007  evlseu  22050  mhpsclcl  22102  mdetunilem7  22574  mdetunilem9  22576  chcoeffeq  22842  cnindis  23248  lmss  23254  lmcls  23258  lmcnp  23260  hausnei  23284  cmpsub  23356  tgcmp  23357  fiuncmp  23360  cmpfi  23364  bwth  23366  1stcrest  23409  2ndcdisj  23412  1stccnp  23418  comppfsc  23488  1stckgenlem  23509  txcls  23560  txcn  23582  txlm  23604  tx1stc  23606  xkococn  23616  hmphdis  23752  ptcmpfi  23769  isfild  23814  fgss2  23830  filconn  23839  trfil2  23843  ufileu  23875  filufint  23876  elfm2  23904  flftg  23952  fclssscls  23974  fclscf  23981  ufilcmp  23988  cnpfcf  23997  alexsubb  24002  alexsubALTlem4  24006  alexsubALT  24007  qustgpopn  24076  tsmsxp  24111  isust  24160  xmettri2  24296  blin2  24385  setsmstopn  24434  met2ndc  24479  metcnp3  24496  tngtopn  24606  reconnlem2  24784  xrge0tsms  24791  fsumcn  24829  bndth  24925  iscmet3lem2  25260  iscmet3  25261  ivthlem1  25420  ivthlem2  25421  ivthlem3  25422  ovolfiniun  25470  volfiniun  25516  ioombl1lem4  25530  ismbf3d  25623  mbfi1flimlem  25691  itg2seq  25711  itgfsum  25796  ellimc3  25848  dvmptfsum  25947  c1liplem1  25969  plypf1  26185  plydivex  26273  aannenlem1  26304  ulmval  26357  ulmcau  26372  ulmbdd  26375  ulmcn  26376  ulmdvlem3  26379  sineq0  26501  efopn  26635  cxpeq  26735  logbgcd1irr  26772  rlimcnp  26943  xrlimcnp  26946  lgsdir2lem2  27305  lgsne0  27314  2lgsoddprm  27395  2sqlem6  27402  2sqlem10  27407  2sqreunnltblem  27430  ltsval2  27636  noetasuplem4  27716  conway  27787  madebdayim  27896  addsass  28013  oncutlt  28272  oniso  28279  addonbday  28287  n0ssoldg  28361  bdayn0p1  28377  oldfib  28385  bdaypw2n0bndlem  28471  bdayfinbndlem1  28475  z12bdaylem1  28478  z12zsodd  28490  axcontlem2  29050  uhgr0vb  29157  uvtx01vtx  29482  uvtxupgrres  29493  fusgrn0degnn0  29585  finsumvtxdg2size  29636  cusgrm1rusgr  29668  wlkv0  29735  wlklenvclwlk  29739  uspgrn2crct  29893  frrusgrord  30428  numclwwlk1lem2fo  30445  isgrpo  30584  grpoidinvlem3  30593  vcdi  30652  vcdir  30653  vcass  30654  nvs  30750  nvtri  30757  blocnilem  30891  chintcli  31418  hsupss  31428  shlej1  31447  elspansn4  31660  spansncvi  31739  hoaddsub  31903  lnopl  32001  lnfnl  32018  riesz4i  32150  pjnormssi  32255  pj3si  32294  stlei  32327  stcltr2i  32362  dmdmd  32387  dmdbr5  32395  mdslmd1lem2  32413  atssma  32465  atcvatlem  32472  chirredlem1  32477  atcvat4i  32484  mdsymlem2  32491  mdsymlem6  32495  sumdmdlem2  32506  cdjreui  32519  elimifd  32629  disjxpin  32674  xrge0infss  32850  expgt0b  32907  xrge0tsmsd  33166  gsumvsca1  33319  gsumvsca2  33320  lmxrge0  34129  ismeas  34376  eulerpartlemb  34545  bnj849  35100  bnj1110  35157  srcmpltd  35255  trssfir1om  35286  fineqvinfep  35300  trssfir1omregs  35311  swrdrevpfx  35330  cusgredgex2  35336  subgrwlk  35345  cusgr3cyclex  35349  umgr2cycllem  35353  umgr2cycl  35354  connpconn  35448  cvmseu  35489  cvmliftlem15  35511  cvmlift2lem1  35515  cvmlift2lem12  35527  satfv0fun  35584  satffunlem  35614  mclsind  35783  r1peuqusdeg1  35856  dfon2lem3  35996  dfon2lem4  35997  dfon2lem6  35999  dfon2lem8  36001  dfon2lem9  36002  hbntg  36016  cgrdegen  36217  funtransport  36244  ifscgr  36257  cgrxfr  36268  brofs2  36290  brifs2  36291  idinside  36297  btwnconn1lem7  36306  btwnconn1lem11  36310  btwnconn1lem12  36311  btwnconn1lem14  36313  broutsideof2  36335  btwnoutside  36338  outsideoftr  36342  in-ax8  36437  ss-ax8  36438  finminlem  36531  ntruni  36540  neibastop1  36572  ontgval  36644  ordtop  36649  ordcmp  36660  onint1  36662  bj-spvew  36873  bj-cbvexvv  36877  bj-ax12w  36916  axc11n11r  36922  bj-ax12v3  36924  bj-nnfan  36989  bj-nnfand  36990  bj-19.42t  37002  bj-sbft  37012  bj-nnflemea  37021  bj-hbaeb2  37060  bj-spcimdv  37137  bj-spcimdvv  37138  bj-sngltag  37225  bj-xtagex  37231  bj-axseprep  37316  bj-0int  37348  bj-ismooredr  37356  bj-inftyexpiinj  37458  nlpfvineqsn  37658  wl-ax13lem1  37743  wl-speqv  37771  wl-sbcom2d  37810  tan2h  37857  ptrest  37864  poimirlem20  37885  poimirlem22  37887  poimirlem26  37891  poimirlem30  37895  poimirlem31  37896  poimirlem32  37897  heicant  37900  voliunnfl  37909  volsupnfl  37910  itg2addnclem2  37917  itg2addnc  37919  itg2gt0cn  37920  ftc2nc  37947  filbcmb  37985  sdclem2  37987  seqpo  37992  nninfnub  37996  neificl  37998  prdstotbnd  38039  cnpwstotbnd  38042  heibor1lem  38054  heibor  38066  bfplem2  38068  opidonOLD  38097  exidu1  38101  grpokerinj  38138  rngoideu  38148  rngodi  38149  rngodir  38150  rngmgmbs4  38176  divrngidl  38273  prnc  38312  rsp3eq  38612  eqvrelqsel  38945  erimeq2  39008  prter2  39251  ax4fromc4  39264  hbae-o  39273  dvelimf-o  39299  ax12indn  39313  ax12inda2  39317  ax12a2-o  39320  l1cvpat  39424  atcvrj0  39798  pmaple  40131  paddasslem5  40194  pclfinN  40270  osumcllem11N  40336  pexmidlem8N  40347  dvheveccl  41482  dihord6apre  41626  lpolconN  41857  lcmineqlem1  42393  oexpreposd  42686  sn-it0e0  42780  cnreeu  42854  eu6w  43028  isnacs3  43061  pellexlem5  43184  pellex  43186  jm2.18  43339  jm2.15nn0  43354  jm2.16nn0  43355  dford3lem2  43378  ttac  43387  onexomgt  43592  onexoegt  43595  omabs2  43683  omcl3g  43685  tfsconcat0b  43697  naddgeoa  43745  safesnsupfiss  43765  rp-isfinite5  43867  cnvssb  43936  clcnvlem  43973  iunrelexpuztr  44069  rfovcnvf1od  44354  ntrrn  44472  nzss  44667  pm11.71  44747  axc11next  44756  hbntal  44903  eel2122old  45067  relwf  45317  modelaxreplem1  45328  ssclaxsep  45332  wfac8prim  45352  fsetsnf1  47406  2reu8i  47467  afvelima  47521  rlimdmafv  47531  rlimdmafv2  47612  elsprel  47829  sfprmdvdsmersenne  47957  perfectALTVlem2  48076  fpprwppr  48093  uhgrimedgi  48244  isuspgrim0lem  48247  uhgrimisgrgric  48285  gpgcubic  48433  gpg5nbgr3star  48435  pgnioedg1  48462  pgnioedg2  48463  pgnioedg3  48464  pgnioedg4  48465  pgnioedg5  48466  copisnmnd  48523  funcringcsetcALTV2lem8  48651  funcringcsetclem8ALTV  48674  lindslinindsimp2lem5  48816  nn0sumshdig  48977  prelrrx2b  49068  itscnhlc0yqe  49113  iscnrm3lem2  49288  diag1f1lem  49659  spd  50031  setrec1lem4  50043  setrec2fun  50045  aacllem  50154