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  203  imbitrdi  251  imbitrrdi  252  biimtrdi  253  biimtrrdi  254  jaoi  857  pm2.37  972  pm2.81  973  oplem1  1056  3jao  1427  impsingle  1627  al2im  1814  exlimdv  1933  19.23v  1942  spimfw  1965  ax13b  2032  nf5-1  2146  hbald  2169  19.8a  2182  spimedv  2198  19.9d  2204  sbequ1  2249  sbft  2270  cbv2w  2335  spimed  2387  cbv2  2402  cbv2h  2405  ax12  2422  axc11n  2425  equvini  2454  sb2  2478  sb4a  2479  mo3  2558  mopick  2619  moexexlem  2620  dvelimdc  2918  necon1ad  2944  necon4bd  2947  rsp2  3256  mo2icl  3693  2reu1  3868  reuss2  4297  reupick2  4302  elpwunsn  4656  pwpw0  4785  sssn  4798  iuneqconst  4975  disjiun  5103  reusv1  5360  reusv3i  5367  ralxfrALT  5378  exneq  5403  opth1  5443  copsexgw  5458  copsexg  5459  opelopabt  5500  solin  5581  wefrc  5640  frinxp  5729  ssrelrn  5866  dmcosseq  5948  reuop  6274  ordunidif  6390  oneqmini  6393  suctr  6428  ordsssuc2  6433  iotan0  6509  fv3  6883  ndmfv  6900  ssimaex  6953  fvopab3ig  6971  iinpreima  7048  fvcofneq  7072  dff3  7079  dff4  7080  ffnfv  7098  fnsnr  7144  fprb  7175  elunirn  7232  f1mpt  7243  isomin  7319  oprabidw  7425  oprabid  7426  mpoeq123  7468  sorpsscmpl  7717  dfwe2  7757  ssorduni  7762  ssonprc  7770  nlimsucg  7826  ordunisuc2  7828  tfinds  7844  ssnlim  7870  f1oweALT  7960  mptcnfimad  7974  el2mpocl  8074  f1o2ndf1  8110  frxp  8114  soxp  8117  poxp2  8131  poxp3  8138  poseq  8146  brtpos  8223  rntpos  8227  dftpos4  8233  onfununi  8319  onnseq  8322  smores2  8332  smo11  8342  tfr3  8376  rdglim2  8409  tz7.48lem  8418  tz7.49  8422  seqomlem2  8428  oawordex  8532  oa00  8534  oaass  8536  om00  8550  odi  8554  omass  8555  oeordi  8562  oelim2  8570  omsmo  8633  eroveu  8789  eceqoveq  8799  map0g  8861  fundmen  9008  sdomdif  9102  onsdominel  9103  pssnn  9145  nneneq  9183  php3  9186  php3OLD  9191  onomeneqOLD  9195  f1finf1o  9234  f1finf1oOLD  9235  findcard3  9247  findcard3OLD  9248  unblem1  9257  fiint  9295  fiintOLD  9296  ixpfi2  9319  dffi2  9392  elfiun  9399  fisup2g  9438  fiinf2g  9471  wemaplem2  9518  preleqALT  9588  inf3lem2  9600  inf3lem3  9601  inf3lem6  9604  noinfep  9631  epfrs  9702  tcmin  9712  r1sdom  9745  tz9.12lem3  9760  rankelb  9795  bndrank  9812  rankunb  9821  rankuni2b  9824  cplem1  9860  karden  9866  carduni  9952  infxpenlem  9984  dfac8alem  10000  alephdom  10052  cardinfima  10068  alephval3  10081  dfac5lem4  10097  dfac5lem5  10098  dfac5lem4OLD  10099  dfac5  10100  dfac2b  10102  kmlem13  10134  nnadju  10169  ackbij1b  10209  cfub  10220  coflim  10232  cflim2  10234  cfslbn  10238  cfslb2n  10239  cofsmo  10240  cfsmolem  10241  sornom  10248  fincssdom  10294  isf32lem1  10324  isf32lem2  10325  isf32lem9  10332  isf34lem4  10348  isfin1-3  10357  axcc4  10410  domtriomlem  10413  axdc2lem  10419  axdc3lem2  10422  zorn2lem4  10470  zorn2lem6  10472  zornn0g  10476  uniimadom  10515  cardmin  10535  ficard  10536  konigthlem  10539  alephreg  10553  cfpwsdom  10555  axextnd  10562  fpwwe2lem5  10606  fpwwe2lem11  10612  fpwwe2lem12  10613  fpwwe2  10614  canthp1lem2  10624  gchpwdom  10641  winalim2  10667  tskuni  10754  grupr  10768  grur1a  10790  axgroth6  10799  grothomex  10800  eltskm  10814  addclpi  10863  nqereu  10900  ltexnq  10946  nsmallnq  10948  genpn0  10974  genpss  10975  genpnmax  10978  ltaddpr  11005  reclem3pr  11020  reclem4pr  11021  suplem1pr  11023  supsrlem  11082  1re  11192  dedekindle  11356  addrid  11372  negn0  11623  negf1o  11624  negfi  12148  sup2  12155  supadd  12167  supmullem1  12169  supmullem2  12170  zmulcl  12598  zeo  12636  uz11  12834  uzwo  12884  eqreznegel  12907  lbzbi  12909  qextlt  13176  qextle  13177  xrsupsslem  13280  xrinfmsslem  13281  supxrun  13289  supxrpnf  13291  supxrunb1  13292  supxrunb2  13293  fzm1  13581  uzrdgfni  13933  hasheqf1oi  14326  hashreshashfun  14414  leisorel  14435  fundmge2nop0  14477  wrdsymb0  14524  swrdnnn0nd  14631  swrdccatin2d  14719  cshinj  14786  repswcshw  14787  rennim  15215  01sqrexlem6  15223  caubnd  15334  sqreulem  15335  caucvgrlem  15646  fsumcvg  15685  supcvg  15829  prodeq2ii  15884  fprodcvg  15903  prodmo  15909  dvdslelem  16285  bitsinv1lem  16417  bitsshft  16451  smuval2  16458  smupvallem  16459  gcdcllem1  16475  bezoutlem2  16516  bezoutlem3  16517  algcvga  16555  isprm3  16659  isprm5  16683  oddprmdvds  16880  vdwlem13  16970  vdwnnlem1  16972  vdwnnlem3  16974  ramub1lem1  17003  prmgaplem5  17032  imasaddfnlem  17497  divsfval  17516  catpropd  17676  joindmss  18344  meetdmss  18358  psdmrn  18538  odlem1  19471  gexlem1  19515  cygctb  19828  rngisomring1  20383  lmodfopnelem1  20810  islss  20846  lspsneq0  20924  lspsneq  21038  psgnodpmr  21505  obselocv  21643  mvrf1  21901  evlseu  21996  mpfrcl  21998  ppttop  22900  epttop  22902  elcls  22966  restntr  23075  cnprest  23182  regsep  23227  nrmsep3  23248  lmmo  23273  cmpsublem  23292  cmpsub  23293  hauscmplem  23299  txcnpi  23501  txcnp  23513  fbun  23733  fbfinnfr  23734  trfbas2  23736  fgcl  23771  filssufilg  23804  ufinffr  23822  isfcls  23902  fclsrest  23917  flimfnfcls  23921  alexsubALTlem2  23941  alexsubALTlem3  23942  alexsubALTlem4  23943  alexsubALT  23944  cnextcn  23960  imasf1oxms  24383  metequiv2  24404  tngngpim  24553  iccpnfcnv  24848  iccpnfhmeo  24849  iscau2  25184  caun0  25188  minveclem3b  25335  itg1climres  25622  mbfi1fseqlem4  25626  ellimc3  25787  limccnp2  25800  dvlip  25905  itgsubstlem  25962  elply2  26108  coefv0  26160  coemulc  26167  ulmss  26313  sineq0  26440  scvxcvx  26903  sqf11  27056  ppiublem1  27120  fsumvma  27131  2sq2  27351  ostth  27557  sltres  27581  nosepdmlem  27602  nocvxminlem  27696  nocvxmin  27697  addsprop  27890  mptelee  28829  brbtwn2  28839  colinearalg  28844  axcontlem4  28901  upgrres1  29247  usgr2trlncl  29697  umgrclwwlkge2  29927  upgr4cycl4dv4e  30121  1to3vfriendship  30217  3cyclfrgrrn1  30221  n4cyclfrgr  30227  frgrncvvdeqlem8  30242  frgrwopreg  30259  2clwwlk2clwwlk  30286  numclwwlk2lem1  30312  frgrreg  30330  frgrogt3nreg  30333  nmcvcn  30631  chlimi  31170  ocsh  31219  shsvs  31259  h1datomi  31517  stcl  32152  stge0  32160  stle1  32161  stm1addi  32181  stm1add3i  32183  cvnsym  32226  mdbr2  32232  dmdbr2  32239  mdsl0  32246  mdsl1i  32257  mdsl2i  32258  cvmdi  32260  atexch  32317  atcvat4i  32333  cdj1i  32369  1arithufdlem4  33526  xrge0iifcnv  33931  esumpr2  34065  sigaclci  34130  cntmeas  34224  mbfmcnt  34267  ballotlemfc0  34492  ballotlemfcc  34493  bnj1379  34828  bnj607  34914  bnj908  34929  bnj938  34935  bnj1174  35001  bnj1280  35018  f1resrcmplf1dlem  35084  fnrelpredd  35087  axnulg  35090  cusgr3cyclex  35125  loop1cycl  35126  acycgrislfgr  35141  pthacycspth  35146  iccllysconn  35239  satffunlem1lem1  35391  satfvel  35401  sate0fv0  35406  funpsstri  35750  fundmpss  35751  dfon2lem3  35770  dfon2lem4  35771  dfon2lem6  35773  dfon2lem9  35776  dfon2  35777  hbimtg  35791  hbaltg  35792  dfrdg4  35936  btwntriv2  35997  btwncomim  35998  btwnswapid  36002  btwnexch3  36005  ifscgr  36029  lineunray  36132  hilbert1.2  36140  cldbnd  36311  tailfb  36362  meran3  36398  arg-ax  36401  ontopbas  36413  onsuct0  36426  limsucncmpi  36430  ordcmp  36432  onint1  36434  weiunpo  36450  bj-syl66ib  36540  bj-gl4  36580  bj-alexim  36612  bj-nfimt  36623  bj-ax6e  36653  bj-hbalt  36666  axc11n11r  36668  bj-nnfim  36731  bj-nnfan  36733  bj-nnfor  36735  bj-nnford  36736  bj-nnflemaa  36747  bj-nnflemae  36749  bj-19.21t  36754  bj-19.23t  36755  bj-19.42t  36758  bj-sbft  36760  bj-hbsb3t  36773  bj-cbv2hv  36782  bj-equsal1t  36807  bj-0int  37086  bj-bary1lem1  37296  topdifinffinlem  37332  isbasisrelowllem1  37340  isbasisrelowllem2  37341  iooelexlt  37347  finorwe  37367  finxpreclem1  37374  finxpreclem2  37375  isinf2  37390  fvineqsneu  37396  fvineqsneq  37397  pibt2  37402  wl-spae  37506  wl-19.8eqv  37508  wl-nfeqfb  37521  wl-mo3t  37561  wl-ax11-lem3  37572  fin2so  37598  poimirlem29  37640  poimirlem30  37641  poimirlem31  37642  poimirlem32  37643  ismblfin  37652  indexdom  37725  fzmul  37732  heibor1lem  37800  heibor  37812  exidu1  37847  rngoideu  37894  zerdivemp1x  37938  ispridl2  38029  cnf1dd  38081  cnf2dd  38082  cnfn1dd  38083  cnfn2dd  38084  orcomdd  38158  disjlem14  38783  disjdmqsss  38787  disjdmqscossss  38788  prtlem14  38859  prter2  38866  aev-o  38916  ax12eq  38926  ax12el  38927  ax12indn  38928  ax12indi  38929  lsatn0  38984  lsatcmp  38988  lsatcv0  39016  lfl1dim  39106  lfl1dim2N  39107  lkrss2N  39154  lub0N  39174  glb0N  39178  glbconxN  39364  hl2at  39391  cvrexchlem  39405  cvratlem  39407  cvrat4  39429  psubspi  39733  pointpsubN  39737  elpaddn0  39786  paddasslem17  39822  ispsubcl2N  39933  ldilval  40099  trlord  40555  diaelrnN  41031  cdlemm10N  41104  cdlemn11pre  41196  dihord2pre  41211  dihglblem2N  41280  dihglblem3N  41281  mapdrvallem2  41631  ioin9i8  42187  sn-sup2  42451  incssnn0  42671  fphpd  42776  rmxycomplete  42878  dford3lem1  42987  iocinico  43173  onsupnmax  43189  cantnfresb  43285  cantnf2  43286  tfsconcatb0  43305  tfsconcat0b  43307  sdomne0  43374  sdomne0d  43375  ensucne0OLD  43491  al3im  43608  brtrclfv2  43688  frege129d  43724  frege60a  43839  frege60c  43884  frege70  43894  rfovcnvf1od  43965  clsk1indlem3  44004  neik0pk1imk0  44008  gneispace  44095  gneispaceel2  44105  gneispacess2  44107  dvconstbi  44295  axc5c4c711toc7  44365  axc5c4c711to11  44366  pm14.24  44393  sbiota1  44395  bi33imp12  44453  bi123imp0  44458  ee233  44481  vk15.4j  44490  ssralv2  44493  alrim3con13v  44495  tratrb  44498  onfrALTlem3  44506  onfrALTlem2  44508  19.41rg  44512  hbimpg  44516  hbalg  44517  ax6e2ndeq  44521  e2  44593  ee223  44596  sspwtrALT  44783  sspwtrALT2  44784  suctrALT2  44798  trintALT  44842  isosctrlem1ALT  44895  relpmin  44914  traxext  44939  modelaxreplem2  44941  ssclaxsep  44944  fnchoice  44995  mptfnd  45208  stoweidlem62  46033  2reu8i  47084  2reuimp  47086  ffnafv  47142  lswn0  47400  reupr  47478  reuopreuprim  47482  requad2  47579  bgoldbnnsum3prm  47760  bgoldbtbndlem2  47762  bgoldbtbndlem4  47764  gricsym  47876  gpgedgvtx1  48008  ply1mulgsumlem2  48305  iunord  49542  setrec2fun  49558