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  1660  al2im  1847  exlimdv  1966  19.23v  1975  spimfw  1998  ax13b  2065  nf5-1  2182  hbald  2205  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  3672  2reu1  3845  reuss2  4272  reupick2  4277  elpwunsn  4645  pwpw0  4774  sssn  4787  iuneqconst  4963  disjiun  5091  trun  5223  reusv1  5362  reusv3i  5369  ralxfrALT  5380  exneq  5411  opth1  5451  copsexgwOLD  5467  copsexg  5468  opelopabt  5510  solin  5590  wefrc  5649  frinxp  5738  ssrelrn  5878  dmcosseq  5962  dmcosseqOLD  5963  reuop  6291  ordunidif  6408  oneqmini  6411  suctr  6446  ordsssuc2  6451  iotan0  6523  fv3  6896  ndmfv  6910  ssimaex  6963  fvopab3ig  6982  iinpreima  7062  fvcofneq  7086  dff3  7093  dff4  7094  ffnfv  7112  fnsnr  7161  fprb  7192  elunirn  7248  f1mpt  7258  f1resrcmplf1dlem  7271  isomin  7338  oprabidw  7444  oprabid  7445  mpoeq123  7485  sorpsscmpl  7735  dfwe2  7773  ssorduni  7778  ssonprc  7786  nlimsucg  7838  ordunisuc2  7840  tfinds  7856  ssnlim  7882  f1oweALT  7969  mptcnfimad  7983  el2mpocl  8083  f1o2ndf1  8119  frxp  8124  soxp  8127  poxp2  8141  poxp3  8148  poseq  8156  brtpos  8233  rntpos  8237  dftpos4  8243  onfununi  8330  onnseq  8333  smores2  8343  smo11  8353  tfr3  8388  rdglim2  8421  tz7.48lem  8430  tz7.49  8434  seqomlem2  8440  oawordex  8544  oa00  8546  oaass  8548  om00  8562  odi  8566  omass  8567  oeordi  8575  oelim2  8583  omsmo  8646  eroveu  8812  eceqoveq  8822  map0g  8891  fundmen  9038  sdomdif  9123  onsdominel  9124  pssnn  9163  nneneq  9200  php3  9203  f1finf1o  9243  findcard3  9253  unblem1  9262  fiint  9296  ixpfi2  9317  dffi2  9393  elfiun  9400  fisup2g  9439  fiinf2g  9472  wemaplem2  9519  elirrv  9569  elirrvOLD  9570  preleqALT  9596  inf3lem2  9608  inf3lem3  9609  inf3lem6  9612  noinfep  9639  epfrs  9710  tcmin  9718  r1sdom  9756  tz9.12lem3  9771  rankelb  9806  bndrank  9823  rankunb  9832  rankuni2b  9835  cplem1  9889  cplem1OLD  9890  kardenOLD  9899  carduni  9986  infxpenlem  10016  dfac8alem  10032  alephdom  10084  cardinfima  10100  alephval3  10113  dfac5lem4  10129  dfac5lem5  10130  dfac5  10131  dfac2b  10133  kmlem13  10165  nnadju  10200  ackbij1b  10240  cfub  10250  coflim  10263  cflim2  10265  cfslbn  10269  cfslb2n  10270  cofsmo  10271  cfsmolem  10272  sornom  10279  fincssdom  10325  isf32lem1  10355  isf32lem2  10356  isf32lem9  10363  isf34lem4  10379  isfin1-3  10388  axcc4  10441  domtriomlem  10444  axdc2lem  10450  axdc3lem2  10453  zorn2lem4  10501  zorn2lem6  10503  zornn0g  10507  uniimadom  10552  cardmin  10572  ficard  10573  konigthlem  10577  alephreg  10591  cfpwsdom  10593  axextnd  10600  fpwwe2lem5  10644  fpwwe2lem11  10650  fpwwe2lem12  10651  fpwwe2  10652  canthp1lem2  10662  gchpwdom  10679  winalim2  10705  tskuni  10792  grupr  10806  grur1a  10828  axgroth6  10837  grothomex  10838  eltskm  10852  addclpi  10901  nqereu  10938  ltexnq  10984  nsmallnq  10986  genpn0  11012  genpss  11013  genpnmax  11016  ltaddpr  11043  reclem3pr  11058  reclem4pr  11059  suplem1pr  11061  supsrlem  11120  1re  11232  dedekindle  11398  addrid  11414  negn0  11667  negf1o  11668  negfi  12188  sup2  12195  supadd  12207  supmullem1  12209  supmullem2  12210  zmulcl  12667  zeo  12707  uz11  12912  uzwo  12960  eqreznegel  12983  lbzbi  12985  qextlt  13255  qextle  13256  xrsupsslem  13359  xrinfmsslem  13360  supxrun  13368  supxrpnf  13370  supxrunb1  13371  supxrunb2  13372  fzm1  13662  uzrdgfni  14022  hasheqf1oi  14415  hashreshashfun  14504  leisorel  14525  fundmge2nop0  14567  wrdsymb0  14614  swrdnnn0nd  14726  swrdccatin2d  14813  cshinj  14882  repswcshw  14883  rennim  15326  01sqrexlem6  15334  caubnd  15446  sqreulem  15447  caucvgrlem  15760  fsumcvg  15798  supcvg  15945  prodeq2ii  16000  fprodcvg  16017  prodmo  16023  dvdslelem  16399  bitsinv1lem  16531  bitsshft  16565  smuval2  16572  smupvallem  16573  gcdcllem1  16589  bezoutlem2  16630  bezoutlem3  16631  algcvga  16669  isprm3  16773  isprm5  16798  oddprmdvds  16995  vdwlem13  17085  vdwnnlem1  17087  vdwnnlem3  17089  ramub1lem1  17118  prmgaplem5  17147  imasaddfnlem  17614  divsfval  17633  catpropd  17797  joindmss  18465  meetdmss  18479  psdmrn  18661  odlem1  19662  gexlem1  19706  cygctb  20019  rngisomring1  20609  lmodfopnelem1  21082  islss  21118  lspsneq0  21196  lspsneq  21309  psgnodpmr  21803  obselocv  21941  mvrf1  22200  evlseu  22299  mpfrcl  22301  ppttop  23232  epttop  23234  elcls  23298  restntr  23407  cnprest  23514  regsep  23559  nrmsep3  23580  lmmo  23605  cmpsublem  23624  cmpsub  23625  hauscmplem  23631  txcnpi  23834  txcnp  23846  fbun  24066  fbfinnfr  24067  trfbas2  24069  fgcl  24104  filssufilg  24137  ufinffr  24155  isfcls  24235  fclsrest  24250  flimfnfcls  24254  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALTlem4  24276  alexsubALT  24277  cnextcn  24293  imasf1oxms  24715  metequiv2  24736  tngngpim  24885  iccpnfcnv  25172  iccpnfhmeo  25173  iscau2  25505  caun0  25509  minveclem3b  25656  itg1climres  25942  mbfi1fseqlem4  25946  ellimc3  26106  limccnp2  26119  dvlip  26220  itgsubstlem  26275  elply2  26421  coefv0  26474  coemulc  26481  ulmss  26633  sineq0  26761  scvxcvx  27222  sqf11  27375  ppiublem1  27438  fsumvma  27449  2sq2  27669  ostth  27875  ltsres  27898  nosepdmlem  27919  nobdaymin  28018  nocvxminlem  28019  addsprop  28241  mpteleeOLD  29352  brbtwn2  29362  colinearalg  29367  axcontlem4  29424  upgrres1  29773  usgr2trlncl  30225  umgrclwwlkge2  30461  loop1cycl  30623  upgr4cycl4dv4e  30665  1to3vfriendship  30761  3cyclfrgrrn1  30765  n4cyclfrgr  30771  frgrncvvdeqlem8  30786  frgrwopreg  30803  2clwwlk2clwwlk  30830  numclwwlk2lem1  30856  frgrreg  30874  frgrogt3nreg  30877  nmcvcn  31176  chlimi  31715  ocsh  31764  shsvs  31804  h1datomi  32062  stcl  32697  stge0  32705  stle1  32706  stm1addi  32726  stm1add3i  32728  cvnsym  32771  mdbr2  32777  dmdbr2  32784  mdsl0  32791  mdsl1i  32802  mdsl2i  32803  cvmdi  32805  atexch  32862  atcvat4i  32878  cdj1i  32914  1arithufdlem4  33957  xrge0iifcnv  34443  esumpr2  34577  sigaclci  34642  cntmeas  34737  mbfmcnt  34779  ballotlemfc0  35004  ballotlemfcc  35005  bnj1379  35339  bnj607  35425  bnj908  35440  bnj938  35446  bnj1174  35512  bnj1280  35529  fnrelpredd  35596  r1filimi  35611  fineqvinfep  35651  tz9.1regs  35660  axsepg2  35666  axsepg4  35669  axnulg  35671  axpowg2  35673  axpowg3  35674  kardcard2b  35691  ackardcard  35693  cusgr3cyclex  35725  acycgrislfgr  35731  pthacycspth  35736  iccllysconn  35829  satffunlem1lem1  35981  satfvel  35991  sate0fv0  35996  antnestlaw2  36271  funpsstri  36345  fundmpss  36346  dfon2lem3  36362  dfon2lem4  36363  dfon2lem6  36365  dfon2lem9  36368  dfon2  36369  hbimtg  36383  hbaltg  36384  dfrdg4  36530  btwntriv2  36592  btwncomim  36593  btwnswapid  36597  btwnexch3  36600  ifscgr  36624  lineunray  36727  hilbert1.2  36735  cldbnd  36945  tailfb  36996  meran3  37032  arg-ax  37035  ontopbas  37047  onsuct0  37060  limsucncmpi  37064  ordcmp  37066  onint1  37068  weiunpo  37084  axtcond  37097  axuntco  37098  dfttc4lem2  37148  bj-bisimpl  37253  bj-bisimpr  37254  bj-syl66ib  37255  bj-gl4  37296  bj-alexim  37341  bj-nfimt  37353  bj-spvw  37365  bj-cbvalvv  37369  bj-ax6e  37398  bj-hbald  37412  axc11n11r  37416  bj-nnfim  37485  bj-nnfan  37487  bj-nnfor  37489  bj-nnford  37490  bj-19.21t  37494  bj-19.23t  37495  bj-19.42t  37498  bj-sbft  37511  bj-nnflemaa  37519  bj-nnflemae  37521  bj-hbsb3t  37531  bj-cbv2hv  37540  bj-equsal1t  37565  bj-axreprepsep  37820  bj-0int  37851  bj-bary1lem1  38063  topdifinffinlem  38101  isbasisrelowllem1  38109  isbasisrelowllem2  38110  iooelexlt  38116  finorwe  38136  finxpreclem1  38143  finxpreclem2  38144  isinf2  38159  fvineqsneu  38165  fvineqsneq  38166  pibt2  38171  wl-spae  38284  wl-19.8eqv  38286  wl-nfeqfb  38299  wl-mo3t  38339  wl-eujustlem1  38351  fin2so  38361  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  poimirlem32  38401  ismblfin  38410  indexdom  38484  fzmul  38491  heibor1lem  38559  heibor  38571  exidu1  38606  rngoideu  38653  zerdivemp1x  38697  ispridl2  38788  cnf1dd  38838  cnf2dd  38839  cnfn1dd  38840  cnfn2dd  38841  orcomdd  38915  disjlem14  39649  disjdmqsss  39653  disjdmqscossss  39654  prtlem14  39747  prter2  39754  aev-o  39804  ax12eq  39814  ax12el  39815  ax12indn  39816  ax12indi  39817  lsatn0  39872  lsatcmp  39876  lsatcv0  39904  lfl1dim  39994  lfl1dim2N  39995  lkrss2N  40042  lub0N  40062  glb0N  40066  glbconxN  40251  hl2at  40278  cvrexchlem  40292  cvratlem  40294  cvrat4  40316  psubspi  40620  pointpsubN  40624  elpaddn0  40673  paddasslem17  40709  ispsubcl2N  40820  ldilval  40986  trlord  41442  diaelrnN  41918  cdlemm10N  41991  cdlemn11pre  42083  dihord2pre  42098  dihglblem2N  42167  dihglblem3N  42168  mapdrvallem2  42518  ioin9i8  43075  sn-sup2  43379  incssnn0  43556  fphpd  43657  rmxycomplete  43758  dford3lem1  43867  iocinico  44053  onsupnmax  44069  cantnfresb  44165  cantnf2  44166  tfsconcatb0  44185  tfsconcat0b  44187  sdomne0  44253  sdomne0d  44254  ensucne0OLD  44370  al3im  44487  brtrclfv2  44567  frege129d  44603  frege60a  44718  frege60c  44763  frege70  44773  rfovcnvf1od  44844  clsk1indlem3  44883  neik0pk1imk0  44887  gneispace  44974  gneispaceel2  44984  gneispacess2  44986  dvconstbi  45158  axc5c4c711toc7  45228  axc5c4c711to11  45229  pm14.24  45256  sbiota1  45258  bi33imp12  45314  bi123imp0  45319  ee233  45342  vk15.4j  45351  ssralv2  45354  alrim3con13v  45356  tratrb  45359  onfrALTlem3  45367  onfrALTlem2  45369  19.41rg  45373  hbimpg  45377  hbalg  45378  ax6e2ndeq  45382  e2  45454  ee223  45457  sspwtrALT  45644  sspwtrALT2  45645  suctrALT2  45659  trintALT  45703  isosctrlem1ALT  45756  relpmin  45775  traxext  45800  modelaxreplem2  45802  ssclaxsep  45805  fnchoice  45863  mptfnd  46071  stoweidlem62  46890  2reu8i  48001  2reuimp  48003  ffnafv  48059  lswn0  48344  reupr  48422  reuopreuprim  48426  requad2  48539  bgoldbnnsum3prm  48720  bgoldbtbndlem2  48722  bgoldbtbndlem4  48724  gricsym  48837  gpgedgvtx1  48978  ply1mulgsumlem2  49317  iunord  50602  setrec2fun  50618