Theorem syl5 35

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 32	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	3	com12 33	1 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl56  37  syl2im  41  imim12i  63  pm2.86d  109  con2d  135  con3d  153  nsyli  158  biimtrid  245  biimtrrid  246  imbitrid  247  adantld  496  adantrd  497  impel  515  mpan9  516  pm4.72  964  pm2.36  985  pm4.79  1021  ecased  1051  alrimdh  1895  stdpc5v  1970  19.37imv  1979  ax12w  2169  ax13dgen2  2174  ax12v  2213  spsd  2223  nf5r  2230  axc4  2351  equs5eALT  2396  ax13lem1  2403  nfeqf  2410  hbae  2460  ax12vALT  2498  2ax6elem  2499  sb1  2507  euimmo  2641  necon2ad  2970  necon4ad  2974  r19.37v  3188  rr19.28v  3621  moeq3  3669  reuimrmo  3702  sbeqalb  3800  srcmpltd  4431  replem  5240  csbexg  5263  ralxfrd  5369  ralxfrd2  5373  ralxfrALT  5376  copsexgwOLD  5460  copsexg  5461  pwssun  5542  somo  5597  ssrel  5758  relssres  6010  dfrn7  6065  cnvssb  6188  dmsnopg  6214  dfco2a  6247  dfpo2  6299  frpoinsg  6346  tz7.7  6388  ordunidif  6413  suctr  6451  trsucss  6453  suc11  6472  imadif  6625  dffv2  6981  fvmptd3f  7010  fvmptnf  7017  foco2  7110  fconst5  7213  fvf1pr  7316  isores3  7344  riotaxfrd  7412  ovmpt4g  7568  ovmpos  7569  ov2gf  7570  ovmpodf  7577  sorpsscmpl  7751  abnexg  7771  onint  7805  limuni3  7864  tfisg  7866  tfis  7867  tfinds  7872  limomss  7883  peano5  7906  fo2ndf  8135  frxp  8141  xpord2pred  8165  xpord2indlem  8167  soseq  8179  suppss2  8221  suppssfv  8223  rntpos  8260  fprlem1  8322  fprresex  8332  wfr3g  8341  onfununi  8353  smofvon2  8368  smo11  8376  smoord  8377  tfrlem11  8400  tz7.44-2  8419  tz7.48lemOLD  8455  tz7.48-1  8457  tz7.49  8459  tz7.49c  8460  omordi  8578  omord  8580  omass  8592  oneo  8593  omeulem1  8594  omopth2  8596  oewordri  8605  oeworde  8606  nnmordi  8644  nnmord  8645  omabs  8664  nnneo  8668  omsmo  8671  naddcllem  8689  qsel  8821  eceqoveq  8847  domunsncan  9100  sbthlem1  9110  2pwuninel  9155  mapen  9164  infensuc  9178  rexdif1en  9180  findcard2  9184  pssnn  9188  ssfi  9192  sucdom2  9222  php  9226  onomeneq  9233  0sdom1dom  9241  sdom1  9245  dif1ennnALT  9272  ac6sfi  9279  frfi  9280  unblem1  9288  unblem2  9289  unbnn2  9293  domunfican  9317  fodomfir  9323  ixpfi2  9343  finsschain  9352  unifi3  9355  marypha1lem  9429  oiexg  9533  brwdom3  9580  inf3lem2  9634  inf3lem3  9635  cantnfval2  9674  cantnflt  9677  cantnflem1  9694  cnfcom  9705  ttrclss  9725  trcl  9733  epfrs  9736  frmin  9757  frinsg  9759  frr3g  9764  frrlem15  9765  r1sdom  9785  setrec1lem4  9975  setrec2fun  9977  cardsdomel  10059  carduni  10066  infpwfien  10145  carduniima  10179  dfac5  10211  dfac12r  10229  dfac12k  10230  kmlem11  10243  djuinf  10271  infxp  10296  cfsuc  10339  cfcoflem  10354  coftr  10355  infpssr  10390  fin23lem30  10424  isf32lem1  10435  isf34lem6  10462  fin1a2lem13  10494  fin1a2s  10496  axcc2lem  10518  domtriomlem  10524  axcclem  10539  ac6num  10561  zorn2lem5  10582  zorn2lem6  10583  axdclem2  10602  alephval2  10661  alephreg  10671  pwcfsdom  10672  axregndlem1  10691  axregnd  10693  axacndlem1  10696  axacndlem2  10697  axacndlem3  10698  axacndlem4  10699  axacnd  10701  gchi  10713  fpwwe2lem12  10731  canthp1  10743  gchpwdom  10759  wunfi  10810  tskwe2  10862  inar1  10864  gruen  10901  intgru  10903  indpi  10996  nqereu  11018  ltbtwnnq  11067  prnmadd  11086  genpcd  11095  prlem934  11122  ltexprlem1  11125  ltexprlem2  11126  ltexprlem7  11131  ltaprlem  11133  ltapr  11134  reclem4pr  11139  suplem2pr  11142  mulcmpblnr  11160  recexsrlem  11192  mulgt0sr  11194  supsrlem  11200  axpre-sup  11258  1re  11312  dedekindle  11478  addlsub  11736  recex  11952  nnunb  12606  0mnnnnn0  12642  prime  12784  zeo  12789  fnn0ind  12802  zindd  12804  btwnz  12806  lbzbi  13067  xrub  13446  elfznelfzo  13912  fvf1tp  13933  addmodlteq  14093  facwordi  14437  fiinfnf1o  14498  hashclb  14506  hashdom  14527  hashf1lem2  14605  seqcoll  14613  brfi1indALT  14659  ccatalpha  14744  pfxccatin12lem2a  14881  swrdrevpfx  14923  limsupbnd2  15656  rlimdm  15724  o1of2  15786  rlimno1  15827  isercoll  15841  caurcvg2  15851  caucvgb  15853  serf0  15854  zsum  15890  fsum2dlem  15942  fsum2d  15943  fsumabs  15974  fsumrlim  15984  fsumo1  15985  fsumiun  15994  zprod  16110  fprod2dlem  16153  fprod2d  16154  odd2np1  16517  ndvdssub  16585  dfgcd2  16725  nprm  16869  maxprmfct  16891  rpexp  16904  pc2dvds  17063  pcfac  17083  unbenlem  17092  4sqlem12  17140  4sqlem17  17145  vdwlem13  17177  prmlem0  17289  mreiincl  17772  sscfn1  17998  initoid  18182  termoid  18183  funcestrcsetclem8  18327  funcsetcestrclem8  18342  pospo  18523  cnvpsb  18759  dirtr  18782  mgmidpfod  18863  mulgaddcom  19314  mulginvcom  19315  gaass  19517  cntz2ss  19555  elsymgbas  19594  symgfix2  19636  pmtrfrn  19678  psgnran  19735  odmulg  19776  odhash3  19796  sylow2alem1  19837  sylow2alem2  19838  pj1eu  19916  efgs1b  19956  efgsfo  19959  efgredlemc  19965  efgredeu  19972  frgpuptinv  19991  lt6abl  20115  ghmcyg  20116  ablfac1eulem  20294  pgpfac1lem5  20301  ablsimpgfindlem1  20329  gsumle  20365  ringinvnz1ne0  20537  irredmul  20665  rnghmsscmap2  20887  rnghmsscmap  20888  rhmsscmap2  20916  rhmsscmap  20917  acsfn1p  21062  lspextmo  21337  lspsncv0  21430  pzriprnglem12  21804  psgnghm  21892  mplcoe1  22352  mplcoe5  22355  evlseu  22398  mhpsclcl  22474  mdetunilem7  22939  mdetunilem9  22941  chcoeffeq  23210  cnindis  23616  lmss  23622  lmcls  23626  lmcnp  23628  hausnei  23652  cmpsub  23724  tgcmp  23725  fiuncmp  23728  cmpfi  23732  bwth  23734  1stcrest  23777  2ndcdisj  23781  1stccnp  23787  comppfsc  23857  1stckgenlem  23878  txcls  23929  txcn  23951  txlm  23973  tx1stc  23975  xkococn  23985  hmphdis  24121  ptcmpfi  24138  isfild  24183  fgss2  24199  filconn  24208  trfil2  24212  ufileu  24244  filufint  24245  elfm2  24273  flftg  24321  fclssscls  24343  fclscf  24350  ufilcmp  24357  cnpfcf  24366  alexsubb  24371  alexsubALTlem4  24375  alexsubALT  24376  qustgpopn  24445  tsmsxp  24480  isust  24529  xmettri2  24665  blin2  24754  setsmstopn  24803  met2ndc  24848  metcnp3  24865  tngtopn  24975  reconnlem2  25153  xrge0tsms  25160  fsumcn  25197  bndth  25285  iscmet3lem2  25619  iscmet3  25620  ivthlem1  25778  ivthlem2  25779  ivthlem3  25780  ovolfiniun  25828  volfiniun  25874  ioombl1lem4  25888  ismbf3d  25981  mbfi1flimlem  26049  itg2seq  26069  itgfsum  26153  ellimc3  26205  dvmptfsum  26301  c1liplem1  26322  plypf1  26537  plydivex  26624  aannenlem1  26661  ulmval  26713  ulmcau  26728  ulmbdd  26731  ulmcn  26732  ulmdvlem3  26735  sineq0  26858  efopn  26992  cxpeq  27091  logbgcd1irr  27128  rlimcnp  27299  xrlimcnp  27302  lgsdir2lem2  27659  lgsne0  27668  2lgsoddprm  27749  2sqlem6  27756  2sqlem10  27761  2sqreunnltblem  27784  ltsval2  28019  noetasuplem4  28099  conway  28171  madebdayim  28280  addsass  28397  oncutlt  28656  oniso  28663  addonbday  28671  n0ssoldg  28745  bdayn0p1  28761  oldfib  28769  bdaypw2n0bndlem  28855  bdayfinbndlem1  28859  z12bdaylem1  28862  z12zsodd  28874  axcontlem2  29549  uhgr0vb  29656  uvtx01vtx  29984  uvtxupgrres  29995  fusgrn0degnn0  30086  finsumvtxdg2size  30137  cusgrm1rusgr  30169  wlkv0  30236  wlklenvclwlk  30240  subgrwlk  30275  uspgrn2crct  30403  umgr2cycllem  30752  umgr2cycl  30753  frrusgrord  30948  numclwwlk1lem2fo  30965  isgrpo  31105  grpoidinvlem3  31114  vcdi  31173  vcdir  31174  vcass  31175  nvs  31271  nvtri  31278  blocnilem  31412  chintcli  31939  hsupss  31949  shlej1  31968  elspansn4  32181  spansncvi  32260  hoaddsub  32424  lnopl  32522  lnfnl  32539  riesz4i  32671  pjnormssi  32776  pj3si  32815  stlei  32848  stcltr2i  32883  dmdmd  32908  dmdbr5  32916  mdslmd1lem2  32934  atssma  32986  atcvatlem  32993  chirredlem1  32998  atcvat4i  33005  mdsymlem2  33012  mdsymlem6  33016  sumdmdlem2  33027  cdjreui  33040  elimifd  33187  disjxpin  33230  xrge0infss  33399  expgt0b  33455  xrge0tsmsd  33681  gsumvsca1  33834  gsumvsca2  33835  lmxrge0  34631  ismeas  34879  eulerpartlemb  35047  bnj849  35602  bnj1110  35659  soinfdom  35769  axprALT2  35787  trssfir1om  35790  acwer1prclem  35816  fineqvinfep  35850  trssfir1omregs  35861  onprcf1acwevdlem1  35965  cusgredgex2  35984  cusgr3cyclex  35988  srepdf  36007  connpconn  36087  cvmseu  36128  cvmliftlem15  36150  cvmlift2lem1  36154  cvmlift2lem12  36166  satfv0fun  36223  satffunlem  36253  mclsind  36422  r1peuqusdeg1  36495  dfon2lem3  36640  dfon2lem4  36641  dfon2lem6  36643  dfon2lem8  36645  dfon2lem9  36646  hbntg  36660  cgrdegen  36862  funtransport  36889  ifscgr  36902  cgrxfr  36913  brofs2  36935  brifs2  36936  idinside  36942  btwnconn1lem7  36951  btwnconn1lem11  36955  btwnconn1lem12  36956  btwnconn1lem14  36958  broutsideof2  36980  btwnoutside  36983  outsideoftr  36987  nmulprop  37032  in-ax8  37106  ss-ax8  37107  finminlem  37199  ntruni  37208  neibastop1  37240  ontgval  37312  ordtop  37317  ordcmp  37328  onint1  37330  bj-alrimdh  37587  bj-spimnfe  37616  bj-spimenfa  37617  bj-cbveximd  37624  bj-spvew  37628  bj-cbvexvv  37632  bj-ax12w  37670  axc11n11r  37678  bj-ax12v3  37680  bj-nnfan  37749  bj-nnfand  37750  bj-19.42t  37760  bj-sbft  37773  bj-nnflemea  37784  bj-hbaeb2  37823  bj-spcimdv  37900  bj-spcimdvv  37901  bj-sngltag  37989  bj-xtagex  37995  bj-axseprep  38083  bj-0int  38115  bj-ismooredr  38123  bj-inftyexpiinj  38224  wl-ax13lem1  38511  wl-speqv  38548  wl-sbcom2d  38587  tan2h  38629  ptrest  38631  poimirlem20  38652  poimirlem22  38654  poimirlem26  38658  poimirlem30  38662  poimirlem31  38663  poimirlem32  38664  heicant  38667  voliunnfl  38676  volsupnfl  38677  itg2addnclem2  38684  itg2addnc  38686  itg2gt0cn  38687  ftc2nc  38714  filbcmb  38768  sdclem2  38770  seqpo  38775  nninfnub  38779  neificl  38781  prdstotbnd  38822  cnpwstotbnd  38825  heibor1lem  38837  heibor  38849  bfplem2  38851  opidonOLD  38880  exidu1  38884  grpokerinj  38921  rngoideu  38931  rngodi  38932  rngodir  38933  rngmgmbs4  38959  divrngidl  39056  prnc  39095  rsp3eq  39393  eqvrelqsel  39726  erimeq2  39789  prter2  40032  ax4fromc4  40045  hbae-o  40054  dvelimf-o  40080  ax12indn  40094  ax12inda2  40098  ax12a2-o  40101  l1cvpat  40205  atcvrj0  40579  pmaple  40912  paddasslem5  40975  pclfinN  41051  osumcllem11N  41117  pexmidlem8N  41128  dvheveccl  42263  dihord6apre  42407  lpolconN  42638  lcmineqlem1  43173  oexpreposd  43473  sn-it0e0  43561  cnreeu  43648  eu6w  43781  isnacs3  43815  pellexlem5  43934  pellex  43936  jm2.18  44089  jm2.15nn0  44104  jm2.16nn0  44105  dford3lem2  44128  ttac  44137  onexomgt  44337  onexoegt  44340  omabs2  44428  omcl3g  44430  tfsconcat0b  44442  naddgeoa  44490  safesnsupfiss  44510  rp-isfinite5  44612  clcnvlem  44717  iunrelexpuztr  44813  rfovcnvf1od  45098  ntrrn  45216  nzss  45395  pm11.71  45475  axc11next  45484  hbntal  45630  eel2122old  45794  cocanss2  46016  relwf  46051  modelaxreplem1  46062  ssclaxsep  46066  wfac8prim  46086  hfrel  46114  fsetsnf1  48216  2reu8i  48277  afvelima  48331  rlimdmafv  48341  rlimdmafv2  48422  elsprel  48651  sfprmdvdsmersenne  48782  perfectALTVlem2  48914  fpprwppr  48931  uhgrimedgi  49082  isuspgrim0lem  49085  uhgrimisgrgric  49123  gpgcubic  49271  gpg5nbgr3star  49273  pgnioedg1  49300  pgnioedg2  49301  pgnioedg3  49302  pgnioedg4  49303  pgnioedg5  49304  copisnmnd  49360  funcringcsetcALTV2lem8  49488  funcringcsetclem8ALTV  49511  lindslinindsimp2lem5  49668  nn0sumshdig  49829  itscnhlc0yqe  49965  iscnrm3lem2  50143  diag1f1lem  50522  spd  50955  aacllem  51108