Theorem syl6 36

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 31	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  syl6com  38  a1dd  51  syl6mpi  68  syl6c  71  syl10  80  com34  92  con1d  146  expi  166  looinv  206  imbitrdi  254  imbitrrdi  255  biimtrdi  256  biimtrrdi  257  jaoi  871  pm2.37  986  pm2.81  987  oplem1  1072  3jao  1452  impsingle  1659  al2im  1846  exlimdv  1965  19.23v  1974  spimfw  1997  ax13b  2064  nf5-1  2181  hbald  2204  19.8a  2217  spimedv  2233  19.9d  2239  sbequ1  2283  sbft  2303  cbv2w  2366  spimed  2417  cbv2  2432  cbv2h  2435  ax12  2452  axc11n  2455  equvini  2484  sb2  2508  sb4a  2509  mo3  2589  mopick  2650  moexexlem  2651  dvelimdc  2946  necon1ad  2972  necon4bd  2975  rsp2  3279  mo2icl  3671  2reu1  3844  reuss2  4271  reupick2  4276  elpwunsn  4644  pwpw0  4773  sssn  4786  iuneqconst  4962  disjiun  5090  trun  5222  reusv1  5358  reusv3i  5365  ralxfrALT  5376  exneq  5403  opth1  5443  copsexgwOLD  5460  copsexg  5461  opelopabt  5505  solin  5585  wefrc  5644  frinxp  5733  ssrelrn  5875  dmcosseq  5959  dmcosseqOLD  5960  reuop  6296  ordunidif  6413  oneqmini  6416  suctr  6451  ordsssuc2  6456  iotan0  6528  fv3  6903  ndmfv  6917  ssimaex  6970  fvopab3ig  6989  iinpreima  7069  fvcofneq  7093  dff3  7100  dff4  7101  ffnfv  7119  fnsnr  7168  fprb  7199  elunirn  7255  f1mpt  7265  f1resrcmplf1dlem  7278  isomin  7345  oprabidw  7451  oprabid  7452  mpoeq123  7492  mpt3fvot2d  7690  sorpsscmpl  7750  dfwe2  7788  ssorduni  7793  ssonprc  7801  nlimsucg  7853  ordunisuc2  7855  tfinds  7871  ssnlim  7897  f1oweALT  7984  mptcnfimad  7998  el2mpocl  8097  f1o2ndf1  8133  frxp  8138  soxp  8141  poxp2  8160  poxp3  8167  poseq  8175  brtpos  8253  rntpos  8257  dftpos4  8263  onfununi  8350  onnseq  8353  smores2  8363  smo11  8373  tfr3  8408  rdglim2  8441  tz7.48lemOLD  8452  tz7.49  8456  seqomlem2  8462  oawordex  8566  oa00  8568  oaass  8570  om00  8584  odi  8588  omass  8589  oeordi  8597  oelim2  8605  omsmo  8668  eroveu  8834  eceqoveq  8844  map0g  8913  fundmen  9060  sdomdif  9145  onsdominel  9146  pssnn  9185  nneneq  9222  php3  9225  f1finf1o  9265  findcard3  9275  unblem1  9285  fiint  9319  ixpfi2  9340  dffi2  9416  elfiun  9423  fisup2g  9462  fiinf2g  9495  wemaplem2  9542  elirrv  9592  elirrvOLD  9593  preleqALT  9619  inf3lem2  9631  inf3lem3  9632  inf3lem6  9635  noinfep  9662  epfrs  9733  tcmin  9741  r1sdom  9782  tz9.12lem3  9797  rankelb  9834  bndrank  9855  rankunb  9865  rankuni2b  9868  r1filimi  9904  cplem1  9951  cplem1OLD  9952  kardenOLD  9961  setrec2fun  9974  carduni  10063  infxpenlem  10093  dfac8alem  10109  alephdom  10161  cardinfima  10177  alephval3  10190  dfac5lem4  10206  dfac5lem5  10207  dfac5  10208  dfac2b  10210  kmlem13  10242  nnadju  10277  ackbij1b  10317  cfub  10327  coflim  10340  cflim2  10342  cfslbn  10346  cfslb2n  10347  cofsmo  10348  cfsmolem  10349  sornom  10356  fincssdom  10402  isf32lem1  10432  isf32lem2  10433  isf32lem9  10440  isf34lem4  10456  isfin1-3  10465  axcc4  10518  domtriomlem  10521  axdc2lem  10527  axdc3lem2  10530  zorn2lem4  10578  zorn2lem6  10580  zornn0g  10584  uniimadom  10629  cardmin  10649  ficard  10650  konigthlem  10654  alephreg  10668  cfpwsdom  10670  axextnd  10677  fpwwe2lem5  10721  fpwwe2lem11  10727  fpwwe2lem12  10728  fpwwe2  10729  canthp1lem2  10739  gchpwdom  10756  winalim2  10782  tskuni  10869  grupr  10883  grur1a  10905  axgroth6  10914  grothomex  10915  eltskm  10929  addclpi  10978  nqereu  11015  ltexnq  11061  nsmallnq  11063  genpn0  11089  genpss  11090  genpnmax  11093  ltaddpr  11120  reclem3pr  11135  reclem4pr  11136  suplem1pr  11138  supsrlem  11197  1re  11309  dedekindle  11475  addrid  11491  negn0  11746  negf1o  11747  negfi  12267  sup2  12274  supadd  12286  supmullem1  12288  supmullem2  12289  zmulcl  12746  zeo  12786  uz11  12991  uzwo  13039  eqreznegel  13062  lbzbi  13064  qextlt  13334  qextle  13335  xrsupsslem  13438  xrinfmsslem  13439  supxrun  13447  supxrpnf  13449  supxrunb1  13450  supxrunb2  13451  fzm1  13742  uzrdgfni  14102  hasheqf1oi  14496  hashreshashfun  14585  leisorel  14606  fundmge2nop0  14648  wrdsymb0  14695  swrdnnn0nd  14807  swrdccatin2d  14894  cshinj  14963  repswcshw  14964  rennim  15407  01sqrexlem6  15415  caubnd  15527  sqreulem  15528  caucvgrlem  15841  fsumcvg  15879  supcvg  16026  prodeq2ii  16081  fprodcvg  16098  prodmo  16104  dvdslelem  16480  bitsinv1lem  16612  bitsshft  16646  smuval2  16653  smupvallem  16654  gcdcllem1  16670  bezoutlem2  16714  bezoutlem3  16715  algcvga  16755  isprm3  16859  isprm5  16884  oddprmdvds  17082  vdwlem13  17172  vdwnnlem1  17174  vdwnnlem3  17176  ramub1lem1  17205  prmgaplem5  17234  imasaddfnlem  17701  divsfval  17720  catpropd  17884  joindmss  18552  meetdmss  18566  psdmrn  18748  odlem1  19750  gexlem1  19794  cygctb  20107  rngisomring1  20699  lmodfopnelem1  21174  islss  21210  lspsneq0  21288  lspsneq  21401  psgnodpmr  21897  obselocv  22035  mvrf1  22294  evlseu  22393  mpfrcl  22395  ppttop  23326  epttop  23328  elcls  23392  restntr  23501  cnprest  23608  regsep  23653  nrmsep3  23674  lmmo  23699  cmpsublem  23718  cmpsub  23719  hauscmplem  23725  txcnpi  23928  txcnp  23940  fbun  24160  fbfinnfr  24161  trfbas2  24163  fgcl  24198  filssufilg  24231  ufinffr  24249  isfcls  24329  fclsrest  24344  flimfnfcls  24348  alexsubALTlem2  24368  alexsubALTlem3  24369  alexsubALTlem4  24370  alexsubALT  24371  cnextcn  24387  imasf1oxms  24809  metequiv2  24830  tngngpim  24979  iccpnfcnv  25266  iccpnfhmeo  25267  iscau2  25599  caun0  25603  minveclem3b  25750  itg1climres  26036  mbfi1fseqlem4  26040  ellimc3  26200  limccnp2  26213  dvlip  26314  itgsubstlem  26369  elply2  26515  coefv0  26568  coemulc  26575  ulmss  26725  sineq0  26853  scvxcvx  27314  sqf11  27467  ppiublem1  27530  fsumvma  27541  2sq2  27761  ostth  27967  ltsres  28020  nosepdmlem  28041  nobdaymin  28140  nocvxminlem  28141  addsprop  28363  mpteleeOLD  29474  brbtwn2  29484  colinearalg  29489  axcontlem4  29546  upgrres1  29895  usgr2trlncl  30347  umgrclwwlkge2  30583  loop1cycl  30745  upgr4cycl4dv4e  30787  1to3vfriendship  30883  3cyclfrgrrn1  30887  n4cyclfrgr  30893  frgrncvvdeqlem8  30908  frgrwopreg  30925  2clwwlk2clwwlk  30952  numclwwlk2lem1  30978  frgrreg  30996  frgrogt3nreg  30999  nmcvcn  31298  chlimi  31837  ocsh  31886  shsvs  31926  h1datomi  32184  stcl  32819  stge0  32827  stle1  32828  stm1addi  32848  stm1add3i  32850  cvnsym  32893  mdbr2  32899  dmdbr2  32906  mdsl0  32913  mdsl1i  32924  mdsl2i  32925  cvmdi  32927  atexch  32984  atcvat4i  33000  cdj1i  33036  1arithufdlem4  34122  xrge0iifcnv  34608  esumpr2  34742  sigaclci  34807  cntmeas  34902  mbfmcnt  34943  ballotlemfc0  35168  ballotlemfcc  35169  bnj1379  35503  bnj607  35589  bnj908  35604  bnj938  35610  bnj1174  35676  bnj1280  35693  ordunmax  35758  soinfdom  35761  fnrelpredd  35765  fineqvinfep  35842  tz9.1regs  35851  axsepg2  35857  axsepg4  35860  axnulg  35862  axpowg2  35864  axpowg3  35865  kardcard2b  35882  ackardcard  35884  j0ltaleph  35940  cusgr3cyclex  35980  acycgrislfgr  35986  pthacycspth  35991  iccllysconn  36084  satffunlem1lem1  36236  satfvel  36246  sate0fv0  36251  antnestlaw2  36526  funpsstri  36606  fundmpss  36607  dfon2lem3  36622  dfon2lem4  36623  dfon2lem6  36625  dfon2lem9  36628  dfon2  36629  hbimtg  36643  hbaltg  36644  dfrdg4  36790  btwntriv2  36852  btwncomim  36853  btwnswapid  36857  btwnexch3  36860  ifscgr  36884  lineunray  36987  hilbert1.2  36995  cldbnd  37189  tailfb  37240  meran3  37276  arg-ax  37279  ontopbas  37291  onsuct0  37304  limsucncmpi  37308  ordcmp  37310  onint1  37312  weiunpo  37328  axtcond  37341  axuntco  37342  dfttc4lem2  37392  bj-bisimpl  37497  bj-bisimpr  37498  bj-syl66ib  37499  bj-gl4  37540  bj-alexim  37585  bj-nfimt  37597  bj-spvw  37609  bj-cbvalvv  37613  bj-ax6e  37642  bj-hbald  37656  axc11n11r  37660  bj-nnfim  37729  bj-nnfan  37731  bj-nnfor  37733  bj-nnford  37734  bj-19.21t  37738  bj-19.23t  37739  bj-19.42t  37742  bj-sbft  37755  bj-nnflemaa  37763  bj-nnflemae  37765  bj-hbsb3t  37775  bj-cbv2hv  37784  bj-equsal1t  37809  bj-axreprepsep  38066  bj-0int  38097  bj-bary1lem1  38308  topdifinffinlem  38346  isbasisrelowllem1  38354  isbasisrelowllem2  38355  iooelexlt  38361  finorwe  38381  finxpreclem1  38388  finxpreclem2  38389  isinf2  38404  fvineqsneu  38410  fvineqsneq  38411  pibt2  38416  wl-spae  38529  wl-19.8eqv  38531  wl-nfeqfb  38544  wl-mo3t  38584  wl-eujustlem1  38596  fin2so  38606  poimirlem29  38643  poimirlem30  38644  poimirlem31  38645  poimirlem32  38646  ismblfin  38655  indexdom  38744  fzmul  38751  heibor1lem  38819  heibor  38831  exidu1  38866  rngoideu  38913  zerdivemp1x  38957  ispridl2  39048  cnf1dd  39098  cnf2dd  39099  cnfn1dd  39100  cnfn2dd  39101  orcomdd  39175  disjlem14  39909  disjdmqsss  39913  disjdmqscossss  39914  prtlem14  40007  prter2  40014  aev-o  40064  ax12eq  40074  ax12el  40075  ax12indn  40076  ax12indi  40077  lsatn0  40132  lsatcmp  40136  lsatcv0  40164  lfl1dim  40254  lfl1dim2N  40255  lkrss2N  40302  lub0N  40322  glb0N  40326  glbconxN  40511  hl2at  40538  cvrexchlem  40552  cvratlem  40554  cvrat4  40576  psubspi  40880  pointpsubN  40884  elpaddn0  40933  paddasslem17  40969  ispsubcl2N  41080  ldilval  41246  trlord  41702  diaelrnN  42178  cdlemm10N  42251  cdlemn11pre  42343  dihord2pre  42358  dihglblem2N  42427  dihglblem3N  42428  mapdrvallem2  42778  ioin9i8  43335  sn-sup2  43631  incssnn0  43798  fphpd  43899  rmxycomplete  44000  dford3lem1  44109  iocinico  44290  onsupnmax  44306  cantnfresb  44402  cantnf2  44403  tfsconcatb0  44422  tfsconcat0b  44424  sdomne0  44490  sdomne0d  44491  ensucne0OLD  44607  al3im  44723  brtrclfv2  44803  frege129d  44839  frege60a  44954  frege60c  44999  frege70  45009  rfovcnvf1od  45080  clsk1indlem3  45119  neik0pk1imk0  45123  gneispace  45210  gneispaceel2  45220  gneispacess2  45222  dvconstbi  45394  axc5c4c711toc7  45464  axc5c4c711to11  45465  pm14.24  45492  sbiota1  45494  bi33imp12  45550  bi123imp0  45555  ee233  45578  vk15.4j  45587  ssralv2  45590  alrim3con13v  45592  tratrb  45595  onfrALTlem3  45603  onfrALTlem2  45605  19.41rg  45609  hbimpg  45613  hbalg  45614  ax6e2ndeq  45618  e2  45690  ee223  45693  sspwtrALT  45880  sspwtrALT2  45881  suctrALT2  45895  trintALT  45939  isosctrlem1ALT  45992  dmstructnn  46002  dmstructfi  46003  relpmin  46018  traxext  46043  modelaxreplem2  46045  ssclaxsep  46048  fnchoice  46122  mptfnd  46330  stoweidlem62  47148  2reu8i  48259  2reuimp  48261  ffnafv  48317  lswn0  48602  reupr  48680  reuopreuprim  48684  requad2  48797  bgoldbnnsum3prm  48978  bgoldbtbndlem2  48980  bgoldbtbndlem4  48982  gricsym  49095  gpgedgvtx1  49236  ply1mulgsumlem2  49575  iunord  50860