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  202  syl6ib  250  syl6ibr  251  syl6bi  252  syl6bir  253  jaoi  853  pm2.37  967  pm2.81  968  oplem1  1053  3jao  1423  impsingle  1631  al2im  1818  exlimdv  1937  19.23v  1946  19.36imvOLD  1950  spimfw  1970  ax13b  2036  nf5-1  2143  hbald  2170  19.8a  2176  spimedv  2193  19.9d  2199  sbequ1  2243  sbft  2265  cbv2w  2336  spimed  2388  cbv2  2403  cbv2h  2406  ax12  2423  axc11n  2426  equvini  2455  sb2  2480  sb4a  2484  mo3  2564  mopick  2627  moexexlem  2628  dvelimdc  2933  necon1ad  2959  necon4bd  2962  rsp2  3136  vtoclgft  3482  mo2icl  3644  2reu1  3826  reuss2  4246  reupick2  4251  elpwunsn  4616  pwpw0  4743  sssn  4756  pwsnOLD  4829  iuneqconst  4932  disjiun  5057  reusv1  5315  reusv3i  5322  ralxfrALT  5333  opth1  5384  copsexgw  5398  copsexg  5399  opelopabt  5438  solin  5519  wefrc  5574  frinxp  5660  ssrelrn  5792  reuop  6185  ordunidif  6299  oneqmini  6302  suctr  6334  ordsssuc2  6339  iotan0  6408  fv3  6774  ndmfv  6786  ssimaex  6835  fvopab3ig  6853  iinpreima  6928  fvcofneq  6951  dff3  6958  dff4  6959  ffnfv  6974  fnsnr  7019  fprb  7051  elunirn  7106  f1mpt  7115  isomin  7188  oprabidw  7286  oprabid  7287  mpoeq123  7325  sorpsscmpl  7565  dfwe2  7602  ssorduni  7606  ssonprc  7614  nlimsucg  7664  ordunisuc2  7666  tfinds  7681  ssnlim  7707  f1oweALT  7788  el2mpocl  7897  f1o2ndf1  7934  frxp  7938  soxp  7941  brtpos  8022  rntpos  8026  dftpos4  8032  onfununi  8143  onnseq  8146  smores2  8156  smo11  8166  tfr3  8201  rdglim2  8234  tz7.48lem  8242  tz7.49  8246  seqomlem2  8252  oawordex  8350  oa00  8352  oaass  8354  om00  8368  odi  8372  omass  8373  oeordi  8380  oelim2  8388  omsmo  8448  eroveu  8559  eceqoveq  8569  map0g  8630  fundmen  8775  sdomdif  8861  onsdominel  8862  nneneq  8896  php3  8899  pssnn  8913  onomeneq  8943  pssnnOLD  8969  f1finf1o  8975  findcard3  8987  unblem1  8996  fiint  9021  ixpfi2  9047  dffi2  9112  elfiun  9119  fisup2g  9157  fiinf2g  9189  wemaplem2  9236  preleqALT  9305  inf3lem2  9317  inf3lem3  9318  inf3lem6  9321  noinfep  9348  dftrpred3g  9412  epfrs  9420  tcmin  9430  r1sdom  9463  tz9.12lem3  9478  rankelb  9513  bndrank  9530  rankunb  9539  rankuni2b  9542  cplem1  9578  karden  9584  carduni  9670  infxpenlem  9700  dfac8alem  9716  alephdom  9768  cardinfima  9784  alephval3  9797  dfac5lem4  9813  dfac5lem5  9814  dfac5  9815  dfac2b  9817  kmlem13  9849  nnadju  9884  ackbij1b  9926  cfub  9936  coflim  9948  cflim2  9950  cfslbn  9954  cfslb2n  9955  cofsmo  9956  cfsmolem  9957  sornom  9964  fincssdom  10010  isf32lem1  10040  isf32lem2  10041  isf32lem9  10048  isf34lem4  10064  isfin1-3  10073  axcc4  10126  domtriomlem  10129  axdc2lem  10135  axdc3lem2  10138  zorn2lem4  10186  zorn2lem6  10188  zornn0g  10192  uniimadom  10231  cardmin  10251  ficard  10252  konigthlem  10255  alephreg  10269  cfpwsdom  10271  axextnd  10278  fpwwe2lem5  10322  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  canthp1lem2  10340  gchpwdom  10357  winalim2  10383  tskuni  10470  grupr  10484  grur1a  10506  axgroth6  10515  grothomex  10516  eltskm  10530  addclpi  10579  nqereu  10616  ltexnq  10662  nsmallnq  10664  genpn0  10690  genpss  10691  genpnmax  10694  ltaddpr  10721  reclem3pr  10736  reclem4pr  10737  suplem1pr  10739  supsrlem  10798  1re  10906  dedekindle  11069  addid1  11085  negn0  11334  negf1o  11335  negfi  11854  sup2  11861  supadd  11873  supmullem1  11875  supmullem2  11876  zmulcl  12299  zeo  12336  uz11  12536  uzwo  12580  eqreznegel  12603  lbzbi  12605  qextlt  12866  qextle  12867  xrsupsslem  12970  xrinfmsslem  12971  supxrun  12979  supxrpnf  12981  supxrunb1  12982  supxrunb2  12983  fzm1  13265  uzrdgfni  13606  hasheqf1oi  13994  hashreshashfun  14082  leisorel  14102  fundmge2nop0  14134  wrdsymb0  14180  swrdnnn0nd  14297  swrdccatin2d  14385  cshinj  14452  repswcshw  14453  rennim  14878  sqrlem6  14887  caubnd  14998  sqreulem  14999  caucvgrlem  15312  fsumcvg  15352  supcvg  15496  prodeq2ii  15551  fprodcvg  15568  prodmo  15574  dvdslelem  15946  bitsinv1lem  16076  bitsshft  16110  smuval2  16117  smupvallem  16118  gcdcllem1  16134  bezoutlem2  16176  bezoutlem3  16177  algcvga  16212  isprm3  16316  isprm5  16340  oddprmdvds  16532  vdwlem13  16622  vdwnnlem1  16624  vdwnnlem3  16626  ramub1lem1  16655  prmgaplem5  16684  imasaddfnlem  17156  divsfval  17175  catpropd  17335  joindmss  18012  meetdmss  18026  psdmrn  18206  odlem1  19058  gexlem1  19099  cygctb  19408  lmodfopnelem1  20074  islss  20111  lspsneq0  20189  lspsneq  20299  psgnodpmr  20707  obselocv  20845  mvrf1  21104  evlseu  21203  mpfrcl  21205  ppttop  22065  epttop  22067  elcls  22132  restntr  22241  cnprest  22348  regsep  22393  nrmsep3  22414  lmmo  22439  cmpsublem  22458  cmpsub  22459  hauscmplem  22465  txcnpi  22667  txcnp  22679  fbun  22899  fbfinnfr  22900  trfbas2  22902  fgcl  22937  filssufilg  22970  ufinffr  22988  isfcls  23068  fclsrest  23083  flimfnfcls  23087  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  cnextcn  23126  imasf1oxms  23551  metequiv2  23572  tngngpim  23729  iccpnfcnv  24013  iccpnfhmeo  24014  iscau2  24346  caun0  24350  minveclem3b  24497  itg1climres  24784  mbfi1fseqlem4  24788  ellimc3  24948  limccnp2  24961  dvlip  25062  itgsubstlem  25117  elply2  25262  coefv0  25314  coemulc  25321  ulmss  25461  sineq0  25585  scvxcvx  26040  sqf11  26193  ppiublem1  26255  fsumvma  26266  2sq2  26486  ostth  26692  mptelee  27166  brbtwn2  27176  colinearalg  27181  axcontlem4  27238  upgrres1  27583  usgr2trlncl  28029  umgrclwwlkge2  28256  upgr4cycl4dv4e  28450  1to3vfriendship  28546  3cyclfrgrrn1  28550  n4cyclfrgr  28556  frgrncvvdeqlem8  28571  frgrwopreg  28588  2clwwlk2clwwlk  28615  numclwwlk2lem1  28641  frgrreg  28659  frgrogt3nreg  28662  nmcvcn  28958  chlimi  29497  ocsh  29546  shsvs  29586  h1datomi  29844  stcl  30479  stge0  30487  stle1  30488  stm1addi  30508  stm1add3i  30510  cvnsym  30553  mdbr2  30559  dmdbr2  30566  mdsl0  30573  mdsl1i  30584  mdsl2i  30585  cvmdi  30587  atexch  30644  atcvat4i  30660  cdj1i  30696  xrge0iifcnv  31785  esumpr2  31935  sigaclci  32000  cntmeas  32094  mbfmcnt  32135  ballotlemfc0  32359  ballotlemfcc  32360  bnj1379  32710  bnj607  32796  bnj908  32811  bnj938  32817  bnj1174  32883  bnj1280  32900  f1resrcmplf1dlem  32958  fnrelpredd  32961  cusgr3cyclex  32998  loop1cycl  32999  acycgrislfgr  33014  pthacycspth  33019  iccllysconn  33112  satffunlem1lem1  33264  satfvel  33274  sate0fv0  33279  funpsstri  33645  fundmpss  33646  dfon2lem3  33667  dfon2lem4  33668  dfon2lem6  33670  dfon2lem9  33673  dfon2  33674  hbimtg  33688  hbaltg  33689  poxp2  33717  poxp3  33723  poseq  33729  sltres  33792  nosepdmlem  33813  nocvxminlem  33899  nocvxmin  33900  dfrdg4  34180  btwntriv2  34241  btwncomim  34242  btwnswapid  34246  btwnexch3  34249  ifscgr  34273  lineunray  34376  hilbert1.2  34384  cldbnd  34442  tailfb  34493  meran3  34529  arg-ax  34532  ontopbas  34544  onsuct0  34557  limsucncmpi  34561  ordcmp  34563  onint1  34565  bj-syl66ib  34662  bj-gl4  34704  bj-alexim  34735  bj-nfimt  34746  bj-ax6e  34776  bj-hbalt  34790  axc11n11r  34792  bj-nnfim  34855  bj-nnfan  34857  bj-nnfor  34859  bj-nnford  34860  bj-nnflemaa  34871  bj-nnflemae  34873  bj-19.21t  34878  bj-19.23t  34879  bj-19.42t  34882  bj-sbft  34884  bj-hbsb3t  34897  bj-cbv2hv  34906  bj-equsal1t  34932  bj-0int  35199  bj-bary1lem1  35409  topdifinffinlem  35445  isbasisrelowllem1  35453  isbasisrelowllem2  35454  iooelexlt  35460  finorwe  35480  finxpreclem1  35487  finxpreclem2  35488  isinf2  35503  fvineqsneu  35509  fvineqsneq  35510  pibt2  35515  wl-spae  35607  wl-19.8eqv  35609  wl-nfeqfb  35622  wl-mo3t  35658  wl-ax11-lem3  35665  fin2so  35691  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  ismblfin  35745  indexdom  35819  fzmul  35826  heibor1lem  35894  heibor  35906  exidu1  35941  rngoideu  35988  zerdivemp1x  36032  ispridl2  36123  cnf1dd  36175  cnf2dd  36176  cnfn1dd  36177  cnfn2dd  36178  orcomdd  36252  prtlem14  36815  prter2  36822  aev-o  36872  ax12eq  36882  ax12el  36883  ax12indn  36884  ax12indi  36885  lsatn0  36940  lsatcmp  36944  lsatcv0  36972  lfl1dim  37062  lfl1dim2N  37063  lkrss2N  37110  lub0N  37130  glb0N  37134  glbconxN  37319  hl2at  37346  cvrexchlem  37360  cvratlem  37362  cvrat4  37384  psubspi  37688  pointpsubN  37692  elpaddn0  37741  paddasslem17  37777  ispsubcl2N  37888  ldilval  38054  trlord  38510  diaelrnN  38986  cdlemm10N  39059  cdlemn11pre  39151  dihord2pre  39166  dihglblem2N  39235  dihglblem3N  39236  mapdrvallem2  39586  ioin9i8  40101  sn-dtru  40116  sn-sup2  40360  incssnn0  40449  fphpd  40554  rmxycomplete  40655  dford3lem1  40764  iocinico  40959  ensucne0OLD  41035  al3im  41144  brtrclfv2  41224  frege129d  41260  frege60a  41375  frege60c  41420  frege70  41430  rfovcnvf1od  41501  clsk1indlem3  41542  neik0pk1imk0  41546  gneispace  41633  gneispaceel2  41643  gneispacess2  41645  dvconstbi  41841  axc5c4c711toc7  41911  axc5c4c711to11  41912  pm14.24  41939  sbiota1  41941  bi33imp12  41999  bi123imp0  42005  ee233  42028  vk15.4j  42037  ssralv2  42040  alrim3con13v  42042  tratrb  42045  onfrALTlem3  42053  onfrALTlem2  42055  19.41rg  42059  hbimpg  42063  hbalg  42064  ax6e2ndeq  42068  e2  42140  ee223  42143  sspwtrALT  42331  sspwtrALT2  42332  suctrALT2  42346  trintALT  42390  isosctrlem1ALT  42443  fnchoice  42461  mptfnd  42675  stoweidlem62  43493  2reu8i  44492  2reuimp  44494  ffnafv  44550  lswn0  44784  reupr  44862  reuopreuprim  44866  requad2  44963  bgoldbnnsum3prm  45144  bgoldbtbndlem2  45146  bgoldbtbndlem4  45148  ply1mulgsumlem2  45616  iunord  46268  setrec2fun  46284