Theorem syl6 35

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)

Hypotheses

Ref	Expression
syl6.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl6.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6

Step	Hyp	Ref	Expression
1		syl6.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6.2	. . 3 ⊢ (𝜒 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 3	sylcom 30	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  syl6com  37  a1dd  50  syl6mpi  67  syl6c  70  syl10  79  com34  91  con1d  145  expi  165  looinv  202  imbitrdi  250  imbitrrdi  251  syl6ibr  252  syl6bi  253  syl6bir  254  jaoi  856  pm2.37  970  pm2.81  971  oplem1  1056  3jao  1426  impsingle  1630  al2im  1817  exlimdv  1937  19.23v  1946  19.36imvOLD  1950  spimfw  1970  ax13b  2036  nf5-1  2142  hbald  2169  19.8a  2175  spimedv  2191  19.9d  2197  sbequ1  2241  sbft  2262  cbv2w  2334  spimed  2388  cbv2  2403  cbv2h  2406  ax12  2423  axc11n  2426  equvini  2455  sb2  2479  sb4a  2480  mo3  2559  mopick  2622  moexexlem  2623  dvelimdc  2931  necon1ad  2958  necon4bd  2961  rsp2  3275  mo2icl  3711  2reu1  3892  reuss2  4316  reupick2  4321  elpwunsn  4688  pwpw0  4817  sssn  4830  pwsnOLD  4902  iuneqconst  5009  disjiun  5136  reusv1  5396  reusv3i  5403  ralxfrALT  5414  exneq  5436  opth1  5476  copsexgw  5491  copsexg  5492  opelopabt  5533  solin  5614  wefrc  5671  frinxp  5759  ssrelrn  5895  reuop  6293  ordunidif  6414  oneqmini  6417  suctr  6451  ordsssuc2  6456  iotan0  6534  fv3  6910  ndmfv  6927  ssimaex  6977  fvopab3ig  6995  iinpreima  7071  fvcofneq  7095  dff3  7102  dff4  7103  ffnfv  7118  fnsnr  7163  fprb  7195  elunirn  7250  f1mpt  7260  isomin  7334  oprabidw  7440  oprabid  7441  mpoeq123  7481  sorpsscmpl  7724  dfwe2  7761  ssorduni  7766  ssonprc  7775  nlimsucg  7831  ordunisuc2  7833  tfinds  7849  ssnlim  7875  f1oweALT  7959  el2mpocl  8072  f1o2ndf1  8108  frxp  8112  soxp  8115  poxp2  8129  poxp3  8136  poseq  8144  brtpos  8220  rntpos  8224  dftpos4  8230  onfununi  8341  onnseq  8344  smores2  8354  smo11  8364  tfr3  8399  rdglim2  8432  tz7.48lem  8441  tz7.49  8445  seqomlem2  8451  oawordex  8557  oa00  8559  oaass  8561  om00  8575  odi  8579  omass  8580  oeordi  8587  oelim2  8595  omsmo  8657  eroveu  8806  eceqoveq  8816  map0g  8878  fundmen  9031  sdomdif  9125  onsdominel  9126  pssnn  9168  nneneq  9209  php3  9212  nneneqOLD  9221  php3OLD  9224  onomeneqOLD  9229  pssnnOLD  9265  f1finf1o  9271  f1finf1oOLD  9272  findcard3  9285  findcard3OLD  9286  unblem1  9295  fiint  9324  ixpfi2  9350  dffi2  9418  elfiun  9425  fisup2g  9463  fiinf2g  9495  wemaplem2  9542  preleqALT  9612  inf3lem2  9624  inf3lem3  9625  inf3lem6  9628  noinfep  9655  epfrs  9726  tcmin  9736  r1sdom  9769  tz9.12lem3  9784  rankelb  9819  bndrank  9836  rankunb  9845  rankuni2b  9848  cplem1  9884  karden  9890  carduni  9976  infxpenlem  10008  dfac8alem  10024  alephdom  10076  cardinfima  10092  alephval3  10105  dfac5lem4  10121  dfac5lem5  10122  dfac5  10123  dfac2b  10125  kmlem13  10157  nnadju  10192  ackbij1b  10234  cfub  10244  coflim  10256  cflim2  10258  cfslbn  10262  cfslb2n  10263  cofsmo  10264  cfsmolem  10265  sornom  10272  fincssdom  10318  isf32lem1  10348  isf32lem2  10349  isf32lem9  10356  isf34lem4  10372  isfin1-3  10381  axcc4  10434  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  zorn2lem4  10494  zorn2lem6  10496  zornn0g  10500  uniimadom  10539  cardmin  10559  ficard  10560  konigthlem  10563  alephreg  10577  cfpwsdom  10579  axextnd  10586  fpwwe2lem5  10630  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  canthp1lem2  10648  gchpwdom  10665  winalim2  10691  tskuni  10778  grupr  10792  grur1a  10814  axgroth6  10823  grothomex  10824  eltskm  10838  addclpi  10887  nqereu  10924  ltexnq  10970  nsmallnq  10972  genpn0  10998  genpss  10999  genpnmax  11002  ltaddpr  11029  reclem3pr  11044  reclem4pr  11045  suplem1pr  11047  supsrlem  11106  1re  11214  dedekindle  11378  addrid  11394  negn0  11643  negf1o  11644  negfi  12163  sup2  12170  supadd  12182  supmullem1  12184  supmullem2  12185  zmulcl  12611  zeo  12648  uz11  12847  uzwo  12895  eqreznegel  12918  lbzbi  12920  qextlt  13182  qextle  13183  xrsupsslem  13286  xrinfmsslem  13287  supxrun  13295  supxrpnf  13297  supxrunb1  13298  supxrunb2  13299  fzm1  13581  uzrdgfni  13923  hasheqf1oi  14311  hashreshashfun  14399  leisorel  14421  fundmge2nop0  14453  wrdsymb0  14499  swrdnnn0nd  14606  swrdccatin2d  14694  cshinj  14761  repswcshw  14762  rennim  15186  01sqrexlem6  15194  caubnd  15305  sqreulem  15306  caucvgrlem  15619  fsumcvg  15658  supcvg  15802  prodeq2ii  15857  fprodcvg  15874  prodmo  15880  dvdslelem  16252  bitsinv1lem  16382  bitsshft  16416  smuval2  16423  smupvallem  16424  gcdcllem1  16440  bezoutlem2  16482  bezoutlem3  16483  algcvga  16516  isprm3  16620  isprm5  16644  oddprmdvds  16836  vdwlem13  16926  vdwnnlem1  16928  vdwnnlem3  16930  ramub1lem1  16959  prmgaplem5  16988  imasaddfnlem  17474  divsfval  17493  catpropd  17653  joindmss  18332  meetdmss  18346  psdmrn  18526  odlem1  19403  gexlem1  19447  cygctb  19760  lmodfopnelem1  20508  islss  20545  lspsneq0  20623  lspsneq  20735  psgnodpmr  21143  obselocv  21283  mvrf1  21545  evlseu  21646  mpfrcl  21648  ppttop  22510  epttop  22512  elcls  22577  restntr  22686  cnprest  22793  regsep  22838  nrmsep3  22859  lmmo  22884  cmpsublem  22903  cmpsub  22904  hauscmplem  22910  txcnpi  23112  txcnp  23124  fbun  23344  fbfinnfr  23345  trfbas2  23347  fgcl  23382  filssufilg  23415  ufinffr  23433  isfcls  23513  fclsrest  23528  flimfnfcls  23532  alexsubALTlem2  23552  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  cnextcn  23571  imasf1oxms  23998  metequiv2  24019  tngngpim  24176  iccpnfcnv  24460  iccpnfhmeo  24461  iscau2  24794  caun0  24798  minveclem3b  24945  itg1climres  25232  mbfi1fseqlem4  25236  ellimc3  25396  limccnp2  25409  dvlip  25510  itgsubstlem  25565  elply2  25710  coefv0  25762  coemulc  25769  ulmss  25909  sineq0  26033  scvxcvx  26490  sqf11  26643  ppiublem1  26705  fsumvma  26716  2sq2  26936  ostth  27142  sltres  27165  nosepdmlem  27186  nocvxminlem  27279  nocvxmin  27280  addsprop  27460  mptelee  28153  brbtwn2  28163  colinearalg  28168  axcontlem4  28225  upgrres1  28570  usgr2trlncl  29017  umgrclwwlkge2  29244  upgr4cycl4dv4e  29438  1to3vfriendship  29534  3cyclfrgrrn1  29538  n4cyclfrgr  29544  frgrncvvdeqlem8  29559  frgrwopreg  29576  2clwwlk2clwwlk  29603  numclwwlk2lem1  29629  frgrreg  29647  frgrogt3nreg  29650  nmcvcn  29948  chlimi  30487  ocsh  30536  shsvs  30576  h1datomi  30834  stcl  31469  stge0  31477  stle1  31478  stm1addi  31498  stm1add3i  31500  cvnsym  31543  mdbr2  31549  dmdbr2  31556  mdsl0  31563  mdsl1i  31574  mdsl2i  31575  cvmdi  31577  atexch  31634  atcvat4i  31650  cdj1i  31686  xrge0iifcnv  32913  esumpr2  33065  sigaclci  33130  cntmeas  33224  mbfmcnt  33267  ballotlemfc0  33491  ballotlemfcc  33492  bnj1379  33841  bnj607  33927  bnj908  33942  bnj938  33948  bnj1174  34014  bnj1280  34031  f1resrcmplf1dlem  34089  fnrelpredd  34092  cusgr3cyclex  34127  loop1cycl  34128  acycgrislfgr  34143  pthacycspth  34148  iccllysconn  34241  satffunlem1lem1  34393  satfvel  34403  sate0fv0  34408  funpsstri  34737  fundmpss  34738  dfon2lem3  34757  dfon2lem4  34758  dfon2lem6  34760  dfon2lem9  34763  dfon2  34764  hbimtg  34778  hbaltg  34779  dfrdg4  34923  btwntriv2  34984  btwncomim  34985  btwnswapid  34989  btwnexch3  34992  ifscgr  35016  lineunray  35119  hilbert1.2  35127  cldbnd  35211  tailfb  35262  meran3  35298  arg-ax  35301  ontopbas  35313  onsuct0  35326  limsucncmpi  35330  ordcmp  35332  onint1  35334  bj-syl66ib  35431  bj-gl4  35473  bj-alexim  35504  bj-nfimt  35515  bj-ax6e  35545  bj-hbalt  35559  axc11n11r  35561  bj-nnfim  35624  bj-nnfan  35626  bj-nnfor  35628  bj-nnford  35629  bj-nnflemaa  35640  bj-nnflemae  35642  bj-19.21t  35647  bj-19.23t  35648  bj-19.42t  35651  bj-sbft  35653  bj-hbsb3t  35666  bj-cbv2hv  35675  bj-equsal1t  35700  bj-0int  35982  bj-bary1lem1  36192  topdifinffinlem  36228  isbasisrelowllem1  36236  isbasisrelowllem2  36237  iooelexlt  36243  finorwe  36263  finxpreclem1  36270  finxpreclem2  36271  isinf2  36286  fvineqsneu  36292  fvineqsneq  36293  pibt2  36298  wl-spae  36390  wl-19.8eqv  36392  wl-nfeqfb  36405  wl-mo3t  36441  wl-ax11-lem3  36449  fin2so  36475  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  ismblfin  36529  indexdom  36602  fzmul  36609  heibor1lem  36677  heibor  36689  exidu1  36724  rngoideu  36771  zerdivemp1x  36815  ispridl2  36906  cnf1dd  36958  cnf2dd  36959  cnfn1dd  36960  cnfn2dd  36961  orcomdd  37035  disjlem14  37668  disjdmqsss  37672  disjdmqscossss  37673  prtlem14  37744  prter2  37751  aev-o  37801  ax12eq  37811  ax12el  37812  ax12indn  37813  ax12indi  37814  lsatn0  37869  lsatcmp  37873  lsatcv0  37901  lfl1dim  37991  lfl1dim2N  37992  lkrss2N  38039  lub0N  38059  glb0N  38063  glbconxN  38249  hl2at  38276  cvrexchlem  38290  cvratlem  38292  cvrat4  38314  psubspi  38618  pointpsubN  38622  elpaddn0  38671  paddasslem17  38707  ispsubcl2N  38818  ldilval  38984  trlord  39440  diaelrnN  39916  cdlemm10N  39989  cdlemn11pre  40081  dihord2pre  40096  dihglblem2N  40165  dihglblem3N  40166  mapdrvallem2  40516  ioin9i8  41024  sn-sup2  41342  incssnn0  41449  fphpd  41554  rmxycomplete  41656  dford3lem1  41765  iocinico  41961  onsupnmax  41977  cantnfresb  42074  cantnf2  42075  tfsconcatb0  42094  tfsconcat0b  42096  sdomne0  42164  sdomne0d  42165  ensucne0OLD  42281  al3im  42398  brtrclfv2  42478  frege129d  42514  frege60a  42629  frege60c  42674  frege70  42684  rfovcnvf1od  42755  clsk1indlem3  42794  neik0pk1imk0  42798  gneispace  42885  gneispaceel2  42895  gneispacess2  42897  dvconstbi  43093  axc5c4c711toc7  43163  axc5c4c711to11  43164  pm14.24  43191  sbiota1  43193  bi33imp12  43251  bi123imp0  43257  ee233  43280  vk15.4j  43289  ssralv2  43292  alrim3con13v  43294  tratrb  43297  onfrALTlem3  43305  onfrALTlem2  43307  19.41rg  43311  hbimpg  43315  hbalg  43316  ax6e2ndeq  43320  e2  43392  ee223  43395  sspwtrALT  43583  sspwtrALT2  43584  suctrALT2  43598  trintALT  43642  isosctrlem1ALT  43695  fnchoice  43713  mptfnd  43945  stoweidlem62  44778  2reu8i  45821  2reuimp  45823  ffnafv  45879  lswn0  46112  reupr  46190  reuopreuprim  46194  requad2  46291  bgoldbnnsum3prm  46472  bgoldbtbndlem2  46474  bgoldbtbndlem4  46476  rngisomring1  46720  ply1mulgsumlem2  47068  iunord  47721  setrec2fun  47737