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  1628  al2im  1815  exlimdv  1934  19.23v  1943  19.36imv  1946  spimfw  1968  ax13b  2039  nf5-1  2149  hbald  2175  19.8a  2180  spimedv  2197  19.9d  2203  sbequ1  2249  sbft  2270  cbv2w  2357  spimed  2406  cbv2  2423  cbv2h  2426  ax12  2445  axc11n  2448  equvini  2477  equviniOLD  2478  sb2  2504  sb4a  2509  sbequiOLD  2534  sbi1OLD  2542  dfsb2ALT  2591  sbftALT  2593  sbequiALT  2596  hbsb2ALT  2599  sbi1ALT  2606  mo3  2648  mopick  2710  moexexlem  2711  dvelimdc  3005  necon1ad  3033  necon4bd  3036  rsp2  3213  vtoclgft  3553  mo2icl  3705  2reu1  3881  reuss2  4283  reupick2  4289  elpwunsn  4621  pwpw0  4746  sssn  4759  pwsnOLD  4831  iuneqconst  4930  dfiun2gOLD  4956  disjiun  5053  reusv1  5298  reusv3i  5305  ralxfrALT  5316  opth1  5367  copsexgw  5381  copsexg  5382  opelopabt  5419  wefrc  5549  frinxp  5634  ssrelrn  5763  reuop  6144  ordunidif  6239  oneqmini  6242  suctr  6274  ordsssuc2  6279  iotan0  6345  fv3  6688  ndmfv  6700  ssimaex  6748  fvopab3ig  6764  iinpreima  6837  fvcofneq  6859  dff3  6866  dff4  6867  ffnfv  6882  fnsnr  6927  fprb  6956  elunirn  7010  f1mpt  7019  isomin  7090  oprabidw  7187  oprabid  7188  mpoeq123  7226  sorpsscmpl  7460  dfwe2  7496  ssorduni  7500  ssonprc  7507  nlimsucg  7557  ordunisuc2  7559  tfinds  7574  ssnlim  7599  f1oweALT  7673  el2mpocl  7781  f1o2ndf1  7818  frxp  7820  soxp  7823  brtpos  7901  rntpos  7905  dftpos4  7911  onfununi  7978  onnseq  7981  smores2  7991  smo11  8001  tfr3  8035  rdglim2  8068  tz7.48lem  8077  tz7.49  8081  seqomlem2  8087  oawordex  8183  oa00  8185  oaass  8187  om00  8201  odi  8205  omass  8206  oeordi  8213  oelim2  8221  omsmo  8281  eroveu  8392  eceqoveq  8402  map0g  8448  fundmen  8583  sdomdif  8665  onsdominel  8666  nneneq  8700  php3  8703  onomeneq  8708  pssnn  8736  f1finf1o  8745  findcard3  8761  unblem1  8770  fiint  8795  ixpfi2  8822  dffi2  8887  elfiun  8894  fisup2g  8932  fiinf2g  8964  wemaplem2  9011  preleqALT  9080  inf3lem2  9092  inf3lem3  9093  inf3lem6  9096  noinfep  9123  epfrs  9173  tcmin  9183  r1sdom  9203  tz9.12lem3  9218  rankelb  9253  bndrank  9270  rankunb  9279  rankuni2b  9282  cplem1  9318  karden  9324  carduni  9410  infxpenlem  9439  dfac8alem  9455  alephdom  9507  cardinfima  9523  alephval3  9536  dfac5lem4  9552  dfac5lem5  9553  dfac5  9554  dfac2b  9556  kmlem13  9588  ackbij1b  9661  cfub  9671  coflim  9683  cflim2  9685  cfslbn  9689  cfslb2n  9690  cofsmo  9691  cfsmolem  9692  sornom  9699  fincssdom  9745  isf32lem1  9775  isf32lem2  9776  isf32lem9  9783  isf34lem4  9799  isfin1-3  9808  axcc4  9861  domtriomlem  9864  axdc2lem  9870  axdc3lem2  9873  zorn2lem4  9921  zorn2lem6  9923  zornn0g  9927  axdclem2  9942  uniimadom  9966  cardmin  9986  ficard  9987  konigthlem  9990  alephreg  10004  cfpwsdom  10006  axextnd  10013  fpwwe2lem6  10057  fpwwe2lem12  10063  fpwwe2lem13  10064  fpwwe2  10065  canthp1lem2  10075  gchpwdom  10092  winalim2  10118  tskuni  10205  grupr  10219  grur1a  10241  axgroth6  10250  grothomex  10251  eltskm  10265  addclpi  10314  nqereu  10351  ltexnq  10397  nsmallnq  10399  genpn0  10425  genpss  10426  genpnmax  10429  ltaddpr  10456  reclem3pr  10471  reclem4pr  10472  suplem1pr  10474  supsrlem  10533  1re  10641  dedekindle  10804  addid1  10820  negn0  11069  negf1o  11070  negfi  11589  fiminreOLD  11590  sup2  11597  supadd  11609  supmullem1  11611  supmullem2  11612  zmulcl  12032  zeo  12069  uz11  12268  uzwo  12312  eqreznegel  12335  lbzbi  12337  qextlt  12597  qextle  12598  xrsupsslem  12701  xrinfmsslem  12702  supxrun  12710  supxrpnf  12712  supxrunb1  12713  supxrunb2  12714  fzm1  12988  uzrdgfni  13327  hasheqf1oi  13713  hashreshashfun  13801  leisorel  13819  fundmge2nop0  13851  wrdsymb0  13901  swrdnnn0nd  14018  swrdccatin2d  14106  cshinj  14173  repswcshw  14174  rennim  14598  sqrlem6  14607  caubnd  14718  sqreulem  14719  caucvgrlem  15029  fsumcvg  15069  supcvg  15211  prodeq2ii  15267  fprodcvg  15284  prodmo  15290  dvdslelem  15659  bitsinv1lem  15790  bitsshft  15824  smuval2  15831  smupvallem  15832  gcdcllem1  15848  bezoutlem2  15888  bezoutlem3  15889  algcvga  15923  isprm3  16027  isprm5  16051  oddprmdvds  16239  vdwlem13  16329  vdwnnlem1  16331  vdwnnlem3  16333  ramub1lem1  16362  prmgaplem5  16391  imasaddfnlem  16801  divsfval  16820  catpropd  16979  joindmss  17617  meetdmss  17631  psdmrn  17817  odlem1  18663  gexlem1  18704  cygctb  19012  lmodfopnelem1  19670  islss  19706  lspsneq0  19784  lspsneq  19894  mvrf1  20205  evlseu  20296  mpfrcl  20298  psgnodpmr  20734  obselocv  20872  ppttop  21615  epttop  21617  elcls  21681  restntr  21790  cnprest  21897  regsep  21942  nrmsep3  21963  lmmo  21988  cmpsublem  22007  cmpsub  22008  hauscmplem  22014  txcnpi  22216  txcnp  22228  fbun  22448  fbfinnfr  22449  trfbas2  22451  fgcl  22486  filssufilg  22519  ufinffr  22537  isfcls  22617  fclsrest  22632  flimfnfcls  22636  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  cnextcn  22675  imasf1oxms  23099  metequiv2  23120  tngngpim  23268  iccpnfcnv  23548  iccpnfhmeo  23549  iscau2  23880  caun0  23884  minveclem3b  24031  itg1climres  24315  mbfi1fseqlem4  24319  ellimc3  24477  limccnp2  24490  dvlip  24590  itgsubstlem  24645  elply2  24786  coefv0  24838  coemulc  24845  ulmss  24985  sineq0  25109  scvxcvx  25563  sqf11  25716  ppiublem1  25778  fsumvma  25789  2sq2  26009  ostth  26215  mptelee  26681  brbtwn2  26691  colinearalg  26696  axcontlem4  26753  upgrres1  27095  usgr2trlncl  27541  umgrclwwlkge2  27769  upgr4cycl4dv4e  27964  1to3vfriendship  28060  3cyclfrgrrn1  28064  n4cyclfrgr  28070  frgrncvvdeqlem8  28085  frgrwopreg  28102  2clwwlk2clwwlk  28129  numclwwlk2lem1  28155  frgrreg  28173  frgrogt3nreg  28176  nmcvcn  28472  chlimi  29011  ocsh  29060  shsvs  29100  h1datomi  29358  stcl  29993  stge0  30001  stle1  30002  stm1addi  30022  stm1add3i  30024  cvnsym  30067  mdbr2  30073  dmdbr2  30080  mdsl0  30087  mdsl1i  30098  mdsl2i  30099  cvmdi  30101  atexch  30158  atcvat4i  30174  cdj1i  30210  xrge0iifcnv  31176  esumpr2  31326  sigaclci  31391  cntmeas  31485  mbfmcnt  31526  ballotlemfc0  31750  ballotlemfcc  31751  bnj1379  32102  bnj607  32188  bnj908  32203  bnj938  32209  bnj1174  32275  bnj1280  32292  f1resrcmplf1dlem  32359  cusgr3cyclex  32383  loop1cycl  32384  acycgrislfgr  32399  pthacycspth  32404  iccllysconn  32497  satffunlem1lem1  32649  satfvel  32659  sate0fv0  32664  funpsstri  33008  fundmpss  33009  dfon2lem3  33030  dfon2lem4  33031  dfon2lem6  33033  dfon2lem9  33036  dfon2  33037  hbimtg  33051  hbaltg  33052  dftrpred3g  33072  poseq  33095  sltres  33169  nosepdmlem  33187  nocvxminlem  33247  nocvxmin  33248  dfrdg4  33412  btwntriv2  33473  btwncomim  33474  btwnswapid  33478  btwnexch3  33481  ifscgr  33505  lineunray  33608  hilbert1.2  33616  cldbnd  33674  tailfb  33725  meran3  33761  arg-ax  33764  ontopbas  33776  onsuct0  33789  limsucncmpi  33793  ordcmp  33795  onint1  33797  bj-syl66ib  33890  bj-gl4  33929  bj-alexim  33960  bj-nfimt  33971  bj-ax6e  34001  bj-hbalt  34015  axc11n11r  34017  bj-nnfim  34075  bj-nnfan  34077  bj-nnfor  34079  bj-nnford  34080  bj-nnflemaa  34091  bj-nnflemae  34093  bj-19.21t  34098  bj-19.23t  34099  bj-19.42t  34102  bj-sbft  34104  bj-hbsb3t  34110  bj-cbv2hv  34119  bj-equsal1t  34145  bj-0int  34396  bj-bary1lem1  34595  topdifinffinlem  34631  isbasisrelowllem1  34639  isbasisrelowllem2  34640  iooelexlt  34646  finorwe  34666  finxpreclem1  34673  finxpreclem2  34674  isinf2  34689  fvineqsneu  34695  fvineqsneq  34696  pibt2  34701  wl-spae  34776  wl-19.8eqv  34778  wl-nfeqfb  34791  wl-mo3t  34827  wl-ax11-lem3  34834  fin2so  34894  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  ismblfin  34948  indexdom  35024  fzmul  35031  heibor1lem  35102  heibor  35114  exidu1  35149  rngoideu  35196  zerdivemp1x  35240  ispridl2  35331  cnf1dd  35383  cnf2dd  35384  cnfn1dd  35385  cnfn2dd  35386  orcomdd  35460  prtlem14  36025  prter2  36032  aev-o  36082  ax12eq  36092  ax12el  36093  ax12indn  36094  ax12indi  36095  lsatn0  36150  lsatcmp  36154  lsatcv0  36182  lfl1dim  36272  lfl1dim2N  36273  lkrss2N  36320  lub0N  36340  glb0N  36344  glbconxN  36529  hl2at  36556  cvrexchlem  36570  cvratlem  36572  cvrat4  36594  psubspi  36898  pointpsubN  36902  elpaddn0  36951  paddasslem17  36987  ispsubcl2N  37098  ldilval  37264  trlord  37720  diaelrnN  38196  cdlemm10N  38269  cdlemn11pre  38361  dihord2pre  38376  dihglblem2N  38445  dihglblem3N  38446  mapdrvallem2  38796  ioin9i8  39119  sn-dtru  39131  incssnn0  39328  fphpd  39433  rmxycomplete  39534  dford3lem1  39643  iocinico  39838  ensucne0OLD  39916  al3im  40011  brtrclfv2  40092  frege129d  40128  frege60a  40244  frege60c  40289  frege70  40299  rfovcnvf1od  40370  clsk1indlem3  40413  neik0pk1imk0  40417  gneispace  40504  gneispaceel2  40514  gneispacess2  40516  dvconstbi  40686  axc5c4c711toc7  40756  axc5c4c711to11  40757  pm14.24  40784  sbiota1  40786  bi33imp12  40844  bi123imp0  40850  ee233  40873  vk15.4j  40882  ssralv2  40885  alrim3con13v  40887  tratrb  40890  onfrALTlem3  40898  onfrALTlem2  40900  19.41rg  40904  hbimpg  40908  hbalg  40909  ax6e2ndeq  40913  e2  40985  ee223  40988  sspwtrALT  41176  sspwtrALT2  41177  suctrALT2  41191  trintALT  41235  isosctrlem1ALT  41288  fnchoice  41306  mptfnd  41532  stoweidlem62  42367  2reu8i  43332  2reuimp  43334  ffnafv  43390  lswn0  43624  reupr  43704  reuopreuprim  43708  requad2  43808  bgoldbnnsum3prm  43989  bgoldbtbndlem2  43991  bgoldbtbndlem4  43993  ply1mulgsumlem2  44461  iunord  44799  setrec2fun  44815