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  1896  stdpc5v  1973  19.37imv  1982  ax12w  2172  ax13dgen2  2177  ax12v  2217  spsd  2227  nf5r  2234  axc4  2355  equs5eALT  2399  ax13lem1  2406  nfeqf  2413  hbae  2463  ax12vALT  2501  2ax6elem  2502  sb1  2510  euimmo  2644  necon2ad  2974  necon4ad  2978  r19.37v  3192  rr19.28v  3625  moeq3  3673  reuimrmo  3706  sbeqalb  3804  srcmpltd  4435  replem  5247  csbexg  5270  ralxfrd  5377  ralxfrd2  5381  ralxfrALT  5384  copsexgwOLD  5468  copsexg  5469  pwssun  5550  somo  5605  ssrelOLD  5768  relssres  6029  dfrn7  6084  cnvssb  6207  dmsnopg  6233  dfco2a  6266  dfpo2  6325  frpoinsg  6372  tz7.7  6414  ordunidif  6439  suctr  6477  trsucss  6479  suc11  6498  imadif  6654  dffv2  7011  fvmptd3f  7040  fvmptnf  7047  foco2  7141  fconst5  7243  fvf1pr  7346  isores3  7374  riotaxfrd  7442  ovmpt4g  7599  ovmpos  7600  ov2gf  7601  ovmpodf  7608  sorpsscmpl  7782  abnexg  7802  onint  7838  limuni3  7897  tfisg  7899  tfis  7900  tfinds  7905  limomss  7916  peano5  7939  fo2ndf  8169  frxp  8175  xpord2pred  8199  xpord2indlem  8201  soseq  8213  suppss2  8255  suppssfv  8257  rntpos  8294  fprlem1  8356  fprresex  8366  wfr3g  8375  onfununi  8387  smofvon2  8402  smo11  8410  smoord  8411  tfrlem11  8434  tz7.44-2  8453  tz7.48lemOLD  8489  tz7.48-1  8491  tz7.49  8493  tz7.49c  8494  omordi  8612  omord  8614  omass  8626  oneo  8627  omeulem1  8628  omopth2  8630  oewordri  8639  oeworde  8640  nnmordi  8678  nnmord  8679  omabs  8698  nnneo  8702  omsmo  8705  naddcllem  8723  qsel  8855  eceqoveq  8881  domunsncan  9134  sbthlem1  9144  2pwuninel  9189  mapen  9198  infensuc  9212  rexdif1en  9214  findcard2  9218  pssnn  9222  ssfi  9226  sucdom2  9256  php  9260  onomeneq  9267  0sdom1dom  9275  sdom1  9279  dif1ennnALT  9306  ac6sfi  9313  frfi  9314  unblem1  9322  unblem2  9323  unbnn2  9327  domunfican  9351  fodomfir  9357  ixpfi2  9377  finsschain  9386  unifi3  9389  marypha1lem  9462  oiexg  9566  brwdom3  9613  inf3lem2  9667  inf3lem3  9668  cantnfval2  9707  cantnflt  9710  cantnflem1  9727  cnfcom  9738  ttrclss  9758  trcl  9766  epfrs  9769  frmin  9790  frinsg  9792  frr3g  9797  frrlem15  9798  r1sdom  9818  setrec1lem4  10008  setrec2fun  10010  cardsdomel  10092  carduni  10101  infpwfien  10180  carduniima  10214  dfac5  10246  dfac12r  10264  dfac12k  10265  kmlem11  10278  djuinf  10306  infxp  10331  cfsuc  10374  cfcoflem  10389  coftr  10390  infpssr  10425  fin23lem30  10459  isf32lem1  10470  isf34lem6  10497  fin1a2lem13  10529  fin1a2s  10531  axcc2lem  10553  domtriomlem  10559  axcclem  10574  ac6num  10596  zorn2lem5  10617  zorn2lem6  10618  axdclem2  10637  alephval2  10696  alephreg  10706  pwcfsdom  10707  axregndlem1  10726  axregnd  10728  axacndlem1  10731  axacndlem2  10732  axacndlem3  10733  axacndlem4  10734  axacnd  10736  gchi  10748  fpwwe2lem12  10766  canthp1  10778  gchpwdom  10794  wunfi  10845  tskwe2  10897  inar1  10899  gruen  10936  intgru  10938  indpi  11031  nqereu  11053  ltbtwnnq  11102  prnmadd  11121  genpcd  11130  prlem934  11157  ltexprlem1  11160  ltexprlem2  11161  ltexprlem7  11166  ltaprlem  11168  ltapr  11169  reclem4pr  11174  suplem2pr  11177  mulcmpblnr  11195  recexsrlem  11227  mulgt0sr  11229  supsrlem  11235  axpre-sup  11293  1re  11347  dedekindle  11513  addlsub  11771  recex  11988  nnunb  12642  0mnnnnn0  12678  prime  12820  zeo  12825  fnn0ind  12838  zindd  12840  btwnz  12842  lbzbi  13103  xrub  13482  elfznelfzo  13948  fvf1tp  13969  addmodlteq  14129  facwordi  14474  fiinfnf1o  14535  hashclb  14543  hashdom  14564  hashf1lem2  14642  seqcoll  14650  brfi1indALT  14696  ccatalpha  14781  pfxccatin12lem2a  14918  swrdrevpfx  14960  limsupbnd2  15694  rlimdm  15762  o1of2  15824  rlimno1  15865  isercoll  15879  caurcvg2  15889  caucvgb  15891  serf0  15892  zsum  15928  fsum2dlem  15980  fsum2d  15981  fsumabs  16012  fsumrlim  16022  fsumo1  16023  fsumiun  16032  zprod  16148  fprod2dlem  16191  fprod2d  16192  odd2np1  16555  ndvdssub  16623  dfgcd2  16763  nprm  16907  maxprmfct  16929  rpexp  16942  pc2dvds  17101  pcfac  17121  unbenlem  17130  4sqlem12  17178  4sqlem17  17183  vdwlem13  17215  prmlem0  17327  mreiincl  17816  sscfn1  18042  initoid  18226  termoid  18227  funcestrcsetclem8  18371  funcsetcestrclem8  18386  pospo  18567  cnvpsb  18803  dirtr  18826  mgmidpfod  18907  mulgaddcom  19358  mulginvcom  19359  gaass  19562  cntz2ss  19600  elsymgbas  19639  symgfix2  19681  pmtrfrn  19723  psgnran  19780  odmulg  19821  odhash3  19841  sylow2alem1  19882  sylow2alem2  19883  pj1eu  19961  efgs1b  20001  efgsfo  20004  efgredlemc  20010  efgredeu  20017  frgpuptinv  20036  lt6abl  20160  ghmcyg  20161  ablfac1eulem  20339  pgpfac1lem5  20346  ablsimpgfindlem1  20374  gsumle  20410  ringinvnz1ne0  20582  irredmul  20710  rnghmsscmap2  20932  rnghmsscmap  20933  rhmsscmap2  20961  rhmsscmap  20962  acsfn1p  21107  lspextmo  21382  lspsncv0  21475  pzriprnglem12  21853  psgnghm  21941  mplcoe1  22401  mplcoe5  22404  evlseu  22447  mhpsclcl  22523  mdetunilem7  22988  mdetunilem9  22990  chcoeffeq  23259  cnindis  23665  lmss  23671  lmcls  23675  lmcnp  23677  hausnei  23701  cmpsub  23773  tgcmp  23774  fiuncmp  23777  cmpfi  23781  bwth  23783  1stcrest  23826  2ndcdisj  23830  1stccnp  23836  comppfsc  23906  1stckgenlem  23927  txcls  23978  txcn  24000  txlm  24022  tx1stc  24024  xkococn  24034  hmphdis  24170  ptcmpfi  24187  isfild  24232  fgss2  24248  filconn  24257  trfil2  24261  ufileu  24293  filufint  24294  elfm2  24322  flftg  24370  fclssscls  24392  fclscf  24399  ufilcmp  24406  cnpfcf  24415  alexsubb  24420  alexsubALTlem4  24424  alexsubALT  24425  qustgpopn  24494  tsmsxp  24529  isust  24578  xmettri2  24714  blin2  24803  setsmstopn  24852  met2ndc  24897  metcnp3  24914  tngtopn  25024  reconnlem2  25202  xrge0tsms  25209  fsumcn  25246  bndth  25334  iscmet3lem2  25668  iscmet3  25669  ivthlem1  25827  ivthlem2  25828  ivthlem3  25829  ovolfiniun  25877  volfiniun  25923  ioombl1lem4  25937  ismbf3d  26030  mbfi1flimlem  26098  itg2seq  26118  itgfsum  26202  ellimc3  26254  dvmptfsum  26350  c1liplem1  26371  plypf1  26586  plydivex  26673  aannenlem1  26712  ulmval  26764  ulmcau  26779  ulmbdd  26782  ulmcn  26783  ulmdvlem3  26786  sineq0  26909  efopn  27043  cxpeq  27142  logbgcd1irr  27179  rlimcnp  27350  xrlimcnp  27353  lgsdir2lem2  27710  lgsne0  27719  2lgsoddprm  27800  2sqlem6  27807  2sqlem10  27812  2sqreunnltblem  27835  ltsval2  28070  noetasuplem4  28150  conway  28222  madebdayim  28331  addsass  28448  oncutlt  28707  oniso  28714  addonbday  28722  n0ssoldg  28796  bdayn0p1  28812  oldfib  28820  bdaypw2n0bndlem  28906  bdayfinbndlem1  28910  z12bdaylem1  28913  z12zsodd  28925  axcontlem2  29600  uhgr0vb  29707  uvtx01vtx  30035  uvtxupgrres  30046  fusgrn0degnn0  30137  finsumvtxdg2size  30188  cusgrm1rusgr  30220  wlkv0  30287  wlklenvclwlk  30291  subgrwlk  30326  uspgrn2crct  30454  umgr2cycllem  30803  umgr2cycl  30804  frrusgrord  30999  numclwwlk1lem2fo  31016  isgrpo  31156  grpoidinvlem3  31165  vcdi  31224  vcdir  31225  vcass  31226  nvs  31322  nvtri  31329  blocnilem  31463  chintcli  31990  hsupss  32000  shlej1  32019  elspansn4  32232  spansncvi  32311  hoaddsub  32475  lnopl  32573  lnfnl  32590  riesz4i  32722  pjnormssi  32827  pj3si  32866  stlei  32899  stcltr2i  32934  dmdmd  32959  dmdbr5  32967  mdslmd1lem2  32985  atssma  33037  atcvatlem  33044  chirredlem1  33049  atcvat4i  33056  mdsymlem2  33063  mdsymlem6  33067  sumdmdlem2  33078  cdjreui  33091  elimifd  33237  disjxpin  33280  xrge0infss  33448  expgt0b  33504  xrge0tsmsd  33733  gsumvsca1  33886  gsumvsca2  33887  lmxrge0  34695  ismeas  34943  eulerpartlemb  35111  bnj849  35666  bnj1110  35723  soinfdom  35841  axprALT2  35857  trssfihf  35860  acwer1prclem  35892  fineqvinfep  35934  trssfihfregs  35945  onprcf1acwevdlem1  36086  cusgredgex2  36105  cusgr3cyclex  36109  srepdf  36128  connpconn  36208  cvmseu  36249  cvmliftlem15  36271  cvmlift2lem1  36275  cvmlift2lem12  36287  satfv0fun  36344  satffunlem  36374  mclsind  36543  r1peuqusdeg1  36616  mirimanofffr  36670  dfon2lem3  36762  dfon2lem4  36763  dfon2lem6  36765  dfon2lem8  36767  dfon2lem9  36768  hbntg  36782  cgrdegen  36984  funtransport  37011  ifscgr  37024  cgrxfr  37035  brofs2  37057  brifs2  37058  idinside  37064  btwnconn1lem7  37073  btwnconn1lem11  37077  btwnconn1lem12  37078  btwnconn1lem14  37080  broutsideof2  37102  btwnoutside  37105  outsideoftr  37109  nmulprop  37154  in-ax8  37228  ss-ax8  37229  finminlem  37321  ntruni  37330  neibastop1  37362  ontgval  37434  ordtop  37439  ordcmp  37450  onint1  37452  bj-alrimdh  37709  bj-spimnfe  37738  bj-spimenfa  37739  bj-cbveximd  37746  bj-spvew  37750  bj-cbvexvv  37754  bj-ax12w  37792  axc11n11r  37800  bj-ax12v3  37802  bj-nnfan  37871  bj-nnfand  37872  bj-19.42t  37882  bj-sbft  37895  bj-nnflemea  37906  bj-hbaeb2  37945  bj-spcimdv  38022  bj-spcimdvv  38023  bj-sngltag  38111  bj-xtagex  38117  cocnv1ssidim  38212  cocnv2ssidim  38215  cossididresb  38227  bj-axseprep  38260  bj-0int  38292  bj-ismooredr  38300  bj-inftyexpiinj  38398  wl-ax13lem1  38685  wl-speqv  38722  wl-sbcom2d  38761  tan2h  38803  ptrest  38805  poimirlem20  38826  poimirlem22  38828  poimirlem26  38832  poimirlem30  38836  poimirlem31  38837  poimirlem32  38838  heicant  38841  voliunnfl  38850  volsupnfl  38851  itg2addnclem2  38858  itg2addnc  38860  itg2gt0cn  38861  ftc2nc  38888  filbcmb  38940  sdclem2  38942  seqpo  38947  nninfnub  38951  neificl  38953  prdstotbnd  38994  cnpwstotbnd  38997  heibor1lem  39009  heibor  39021  bfplem2  39023  opidonOLD  39052  exidu1  39056  grpokerinj  39093  rngoideu  39103  rngodi  39104  rngodir  39105  rngmgmbs4  39131  divrngidl  39228  prnc  39267  rsp3eq  39565  eqvrelqsel  39898  erimeq2  39961  prter2  40204  ax4fromc4  40217  hbae-o  40226  dvelimf-o  40252  ax12indn  40266  ax12inda2  40270  ax12a2-o  40273  l1cvpat  40377  atcvrj0  40751  pmaple  41084  paddasslem5  41147  pclfinN  41223  osumcllem11N  41289  pexmidlem8N  41300  dvheveccl  42435  dihord6apre  42579  lpolconN  42810  lcmineqlem1  43345  oexpreposd  43645  sn-it0e0  43733  cnreeu  43820  eu6w  43953  isnacs3  43987  pellexlem5  44106  pellex  44108  jm2.18  44261  jm2.15nn0  44276  jm2.16nn0  44277  dford3lem2  44300  ttac  44309  onexomgt  44504  onexoegt  44507  omabs2  44595  omcl3g  44597  tfsconcat0b  44609  naddgeoa  44657  safesnsupfiss  44677  rp-isfinite5  44779  clcnvlem  44884  iunrelexpuztr  44980  rfovcnvf1od  45265  ntrrn  45383  nzss  45562  pm11.71  45642  axc11next  45651  hbntal  45796  eel2122old  45960  cocanss2  46183  relwf  46221  modelaxreplem1  46232  ssclaxsep  46236  wfac8prim  46256  hfrel  46284  fsetsnf1  48395  2reu8i  48457  afvelima  48510  rlimdmafv  48520  rlimdmafv2  48601  elsprel  48830  sfprmdvdsmersenne  48961  perfectALTVlem2  49093  fpprwppr  49110  uhgrimedgi  49261  isuspgrim0lem  49264  uhgrimisgrgric  49302  gpgcubic  49450  gpg5nbgr3star  49452  pgnioedg1  49479  pgnioedg2  49480  pgnioedg3  49481  pgnioedg4  49482  pgnioedg5  49483  copisnmnd  49539  funcringcsetcALTV2lem8  49667  funcringcsetclem8ALTV  49690  azcn  49720  lindslinindsimp2lem5  49905  nn0sumshdig  50066  itscnhlc0yqe  50202  iscnrm3lem2  50380  diag1f1lem  50759  spd  51192  aacllem  51367