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  147  expi  167  looinv  205  syl6ib  253  syl6ibr  254  syl6bi  255  syl6bir  256  jaoi  853  pm2.37  967  pm2.81  968  oplem1  1051  3jao  1421  impsingle  1627  al2im  1814  exlimdv  1933  19.23v  1942  19.36imv  1945  spimfw  1967  ax13b  2038  nf5-1  2148  hbald  2174  19.8a  2179  spimedv  2196  19.9d  2202  sbequ1  2248  sbft  2269  cbv2w  2356  spimed  2405  cbv2  2422  cbv2h  2425  ax12  2444  axc11n  2447  equvini  2476  equviniOLD  2477  sb2  2503  sb4a  2508  sbequiOLD  2533  sbi1OLD  2541  dfsb2ALT  2590  sbftALT  2592  sbequiALT  2595  hbsb2ALT  2598  sbi1ALT  2605  mo3  2647  mopick  2709  moexexlem  2710  dvelimdc  3008  necon1ad  3036  necon4bd  3039  rsp2  3216  vtoclgft  3556  mo2icl  3708  2reu1  3884  reuss2  4286  reupick2  4292  elpwunsn  4624  pwpw0  4749  sssn  4762  pwsnOLD  4834  iuneqconst  4933  dfiun2gOLD  4959  disjiun  5056  reusv1  5301  reusv3i  5308  ralxfrALT  5319  opth1  5370  copsexgw  5384  copsexg  5385  opelopabt  5422  wefrc  5552  frinxp  5637  ssrelrn  5766  reuop  6147  ordunidif  6242  oneqmini  6245  suctr  6277  ordsssuc2  6282  iotan0  6348  fv3  6691  ndmfv  6703  ssimaex  6751  fvopab3ig  6767  iinpreima  6840  fvcofneq  6862  dff3  6869  dff4  6870  ffnfv  6885  fnsnr  6930  fprb  6959  elunirn  7013  f1mpt  7022  isomin  7093  oprabidw  7190  oprabid  7191  mpoeq123  7229  sorpsscmpl  7463  dfwe2  7499  ssorduni  7503  ssonprc  7510  nlimsucg  7560  ordunisuc2  7562  tfinds  7577  ssnlim  7602  f1oweALT  7676  el2mpocl  7784  f1o2ndf1  7821  frxp  7823  soxp  7826  brtpos  7904  rntpos  7908  dftpos4  7914  onfununi  7981  onnseq  7984  smores2  7994  smo11  8004  tfr3  8038  rdglim2  8071  tz7.48lem  8080  tz7.49  8084  seqomlem2  8090  oawordex  8186  oa00  8188  oaass  8190  om00  8204  odi  8208  omass  8209  oeordi  8216  oelim2  8224  omsmo  8284  eroveu  8395  eceqoveq  8405  map0g  8451  fundmen  8586  sdomdif  8668  onsdominel  8669  nneneq  8703  php3  8706  onomeneq  8711  pssnn  8739  f1finf1o  8748  findcard3  8764  unblem1  8773  fiint  8798  ixpfi2  8825  dffi2  8890  elfiun  8897  fisup2g  8935  fiinf2g  8967  wemaplem2  9014  preleqALT  9083  inf3lem2  9095  inf3lem3  9096  inf3lem6  9099  noinfep  9126  epfrs  9176  tcmin  9186  r1sdom  9206  tz9.12lem3  9221  rankelb  9256  bndrank  9273  rankunb  9282  rankuni2b  9285  cplem1  9321  karden  9327  carduni  9413  infxpenlem  9442  dfac8alem  9458  alephdom  9510  cardinfima  9526  alephval3  9539  dfac5lem4  9555  dfac5lem5  9556  dfac5  9557  dfac2b  9559  kmlem13  9591  ackbij1b  9664  cfub  9674  coflim  9686  cflim2  9688  cfslbn  9692  cfslb2n  9693  cofsmo  9694  cfsmolem  9695  sornom  9702  fincssdom  9748  isf32lem1  9778  isf32lem2  9779  isf32lem9  9786  isf34lem4  9802  isfin1-3  9811  axcc4  9864  domtriomlem  9867  axdc2lem  9873  axdc3lem2  9876  zorn2lem4  9924  zorn2lem6  9926  zornn0g  9930  axdclem2  9945  uniimadom  9969  cardmin  9989  ficard  9990  konigthlem  9993  alephreg  10007  cfpwsdom  10009  axextnd  10016  fpwwe2lem6  10060  fpwwe2lem12  10066  fpwwe2lem13  10067  fpwwe2  10068  canthp1lem2  10078  gchpwdom  10095  winalim2  10121  tskuni  10208  grupr  10222  grur1a  10244  axgroth6  10253  grothomex  10254  eltskm  10268  addclpi  10317  nqereu  10354  ltexnq  10400  nsmallnq  10402  genpn0  10428  genpss  10429  genpnmax  10432  ltaddpr  10459  reclem3pr  10474  reclem4pr  10475  suplem1pr  10477  supsrlem  10536  1re  10644  dedekindle  10807  addid1  10823  negn0  11072  negf1o  11073  negfi  11592  fiminreOLD  11593  sup2  11600  supadd  11612  supmullem1  11614  supmullem2  11615  zmulcl  12034  zeo  12071  uz11  12270  uzwo  12314  eqreznegel  12337  lbzbi  12339  qextlt  12599  qextle  12600  xrsupsslem  12703  xrinfmsslem  12704  supxrun  12712  supxrpnf  12714  supxrunb1  12715  supxrunb2  12716  fzm1  12990  uzrdgfni  13329  hasheqf1oi  13715  hashreshashfun  13803  leisorel  13821  fundmge2nop0  13853  wrdsymb0  13904  swrdnnn0nd  14021  swrdccatin2d  14109  cshinj  14176  repswcshw  14177  rennim  14601  sqrlem6  14610  caubnd  14721  sqreulem  14722  caucvgrlem  15032  fsumcvg  15072  supcvg  15214  prodeq2ii  15270  fprodcvg  15287  prodmo  15293  dvdslelem  15662  bitsinv1lem  15793  bitsshft  15827  smuval2  15834  smupvallem  15835  gcdcllem1  15851  bezoutlem2  15891  bezoutlem3  15892  algcvga  15926  isprm3  16030  isprm5  16054  oddprmdvds  16242  vdwlem13  16332  vdwnnlem1  16334  vdwnnlem3  16336  ramub1lem1  16365  prmgaplem5  16394  imasaddfnlem  16804  divsfval  16823  catpropd  16982  joindmss  17620  meetdmss  17634  psdmrn  17820  odlem1  18666  gexlem1  18707  cygctb  19015  lmodfopnelem1  19673  islss  19709  lspsneq0  19787  lspsneq  19897  mvrf1  20208  evlseu  20299  mpfrcl  20301  psgnodpmr  20737  obselocv  20875  ppttop  21618  epttop  21620  elcls  21684  restntr  21793  cnprest  21900  regsep  21945  nrmsep3  21966  lmmo  21991  cmpsublem  22010  cmpsub  22011  hauscmplem  22017  txcnpi  22219  txcnp  22231  fbun  22451  fbfinnfr  22452  trfbas2  22454  fgcl  22489  filssufilg  22522  ufinffr  22540  isfcls  22620  fclsrest  22635  flimfnfcls  22639  alexsubALTlem2  22659  alexsubALTlem3  22660  alexsubALTlem4  22661  alexsubALT  22662  cnextcn  22678  imasf1oxms  23102  metequiv2  23123  tngngpim  23271  iccpnfcnv  23551  iccpnfhmeo  23552  iscau2  23883  caun0  23887  minveclem3b  24034  itg1climres  24318  mbfi1fseqlem4  24322  ellimc3  24480  limccnp2  24493  dvlip  24593  itgsubstlem  24648  elply2  24789  coefv0  24841  coemulc  24848  ulmss  24988  sineq0  25112  scvxcvx  25566  sqf11  25719  ppiublem1  25781  fsumvma  25792  2sq2  26012  ostth  26218  mptelee  26684  brbtwn2  26694  colinearalg  26699  axcontlem4  26756  upgrres1  27098  usgr2trlncl  27544  umgrclwwlkge2  27772  upgr4cycl4dv4e  27967  1to3vfriendship  28063  3cyclfrgrrn1  28067  n4cyclfrgr  28073  frgrncvvdeqlem8  28088  frgrwopreg  28105  2clwwlk2clwwlk  28132  numclwwlk2lem1  28158  frgrreg  28176  frgrogt3nreg  28179  nmcvcn  28475  chlimi  29014  ocsh  29063  shsvs  29103  h1datomi  29361  stcl  29996  stge0  30004  stle1  30005  stm1addi  30025  stm1add3i  30027  cvnsym  30070  mdbr2  30076  dmdbr2  30083  mdsl0  30090  mdsl1i  30101  mdsl2i  30102  cvmdi  30104  atexch  30161  atcvat4i  30177  cdj1i  30213  xrge0iifcnv  31180  esumpr2  31330  sigaclci  31395  cntmeas  31489  mbfmcnt  31530  ballotlemfc0  31754  ballotlemfcc  31755  bnj1379  32106  bnj607  32192  bnj908  32207  bnj938  32213  bnj1174  32279  bnj1280  32296  f1resrcmplf1dlem  32363  cusgr3cyclex  32387  loop1cycl  32388  acycgrislfgr  32403  pthacycspth  32408  iccllysconn  32501  satffunlem1lem1  32653  satfvel  32663  sate0fv0  32668  funpsstri  33012  fundmpss  33013  dfon2lem3  33034  dfon2lem4  33035  dfon2lem6  33037  dfon2lem9  33040  dfon2  33041  hbimtg  33055  hbaltg  33056  dftrpred3g  33076  poseq  33099  sltres  33173  nosepdmlem  33191  nocvxminlem  33251  nocvxmin  33252  dfrdg4  33416  btwntriv2  33477  btwncomim  33478  btwnswapid  33482  btwnexch3  33485  ifscgr  33509  lineunray  33612  hilbert1.2  33620  cldbnd  33678  tailfb  33729  meran3  33765  arg-ax  33768  ontopbas  33780  onsuct0  33793  limsucncmpi  33797  ordcmp  33799  onint1  33801  bj-syl66ib  33894  bj-gl4  33933  bj-alexim  33964  bj-nfimt  33975  bj-ax6e  34005  bj-hbalt  34019  axc11n11r  34021  bj-nnfim  34079  bj-nnfan  34081  bj-nnfor  34083  bj-nnford  34084  bj-nnflemaa  34095  bj-nnflemae  34097  bj-19.21t  34102  bj-19.23t  34103  bj-19.42t  34106  bj-sbft  34108  bj-hbsb3t  34114  bj-cbv2hv  34123  bj-equsal1t  34149  bj-0int  34397  bj-bary1lem1  34596  topdifinffinlem  34632  isbasisrelowllem1  34640  isbasisrelowllem2  34641  iooelexlt  34647  finorwe  34667  finxpreclem1  34674  finxpreclem2  34675  isinf2  34690  fvineqsneu  34696  fvineqsneq  34697  pibt2  34702  wl-spae  34765  wl-19.8eqv  34767  wl-nfeqfb  34780  wl-mo3t  34816  wl-ax11-lem3  34823  fin2so  34883  poimirlem29  34925  poimirlem30  34926  poimirlem31  34927  poimirlem32  34928  ismblfin  34937  indexdom  35013  fzmul  35020  heibor1lem  35091  heibor  35103  exidu1  35138  rngoideu  35185  zerdivemp1x  35229  ispridl2  35320  cnf1dd  35372  cnf2dd  35373  cnfn1dd  35374  cnfn2dd  35375  orcomdd  35449  prtlem14  36014  prter2  36021  aev-o  36071  ax12eq  36081  ax12el  36082  ax12indn  36083  ax12indi  36084  lsatn0  36139  lsatcmp  36143  lsatcv0  36171  lfl1dim  36261  lfl1dim2N  36262  lkrss2N  36309  lub0N  36329  glb0N  36333  glbconxN  36518  hl2at  36545  cvrexchlem  36559  cvratlem  36561  cvrat4  36583  psubspi  36887  pointpsubN  36891  elpaddn0  36940  paddasslem17  36976  ispsubcl2N  37087  ldilval  37253  trlord  37709  diaelrnN  38185  cdlemm10N  38258  cdlemn11pre  38350  dihord2pre  38365  dihglblem2N  38434  dihglblem3N  38435  mapdrvallem2  38785  ioin9i8  39105  sn-dtru  39117  incssnn0  39314  fphpd  39419  rmxycomplete  39520  dford3lem1  39629  iocinico  39824  ensucne0OLD  39902  al3im  39997  brtrclfv2  40078  frege129d  40114  frege60a  40230  frege60c  40275  frege70  40285  rfovcnvf1od  40356  clsk1indlem3  40399  neik0pk1imk0  40403  gneispace  40490  gneispaceel2  40500  gneispacess2  40502  dvconstbi  40672  axc5c4c711toc7  40742  axc5c4c711to11  40743  pm14.24  40770  sbiota1  40772  bi33imp12  40830  bi123imp0  40836  ee233  40859  vk15.4j  40868  ssralv2  40871  alrim3con13v  40873  tratrb  40876  onfrALTlem3  40884  onfrALTlem2  40886  19.41rg  40890  hbimpg  40894  hbalg  40895  ax6e2ndeq  40899  e2  40971  ee223  40974  sspwtrALT  41162  sspwtrALT2  41163  suctrALT2  41177  trintALT  41221  isosctrlem1ALT  41274  fnchoice  41292  mptfnd  41518  stoweidlem62  42354  2reu8i  43319  2reuimp  43321  ffnafv  43377  lswn0  43611  reupr  43691  reuopreuprim  43695  requad2  43795  bgoldbnnsum3prm  43976  bgoldbtbndlem2  43978  bgoldbtbndlem4  43980  ply1mulgsumlem2  44448  iunord  44786  setrec2fun  44802