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 ⊢ (𝜑 → (𝜓 → 𝜃))

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  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  870  pm2.37  986  pm2.81  987  oplem1  1070  3jao  1448  impsingle  1650  al2im  1837  exlimdv  1956  19.23v  1965  spimfw  1988  ax13b  2055  nf5-1  2182  hbald  2205  19.8a  2219  spimedv  2235  19.9d  2241  sbequ1  2286  sbft  2307  cbv2w  2371  spimed  2422  cbv2  2437  cbv2h  2440  ax12  2457  axc11n  2460  equvini  2489  sb2  2513  sb4a  2514  mo3  2594  mopick  2655  moexexlem  2656  dvelimdc  2951  necon1ad  2977  necon4bd  2980  rsp2  3282  mo2icl  3680  2reu1  3853  reuss2  4281  reupick2  4286  elpwunsn  4646  pwpw0  4774  sssn  4787  iuneqconst  4964  disjiun  5093  trun  5223  reusv1  5359  reusv3i  5366  ralxfrALT  5377  exneq  5408  opth1  5448  copsexgwOLD  5464  copsexg  5465  opelopabt  5507  solin  5587  wefrc  5646  frinxp  5735  ssrelrn  5875  dmcosseq  5959  dmcosseqOLD  5960  reuop  6284  ordunidif  6400  oneqmini  6403  suctr  6438  ordsssuc2  6443  iotan0  6515  fv3  6889  ndmfv  6903  ssimaex  6956  fvopab3ig  6975  iinpreima  7054  fvcofneq  7078  dff3  7085  dff4  7086  ffnfv  7104  fnsnr  7151  fprb  7182  elunirn  7239  f1mpt  7249  isomin  7325  oprabidw  7431  oprabid  7432  mpoeq123  7472  sorpsscmpl  7721  dfwe2  7761  ssorduni  7766  ssonprc  7774  nlimsucg  7826  ordunisuc2  7828  tfinds  7844  ssnlim  7870  f1oweALT  7957  mptcnfimad  7971  el2mpocl  8069  f1o2ndf1  8105  frxp  8110  soxp  8113  poxp2  8127  poxp3  8134  poseq  8142  brtpos  8219  rntpos  8223  dftpos4  8229  onfununi  8316  onnseq  8319  smores2  8329  smo11  8339  tfr3  8374  rdglim2  8407  tz7.48lem  8416  tz7.49  8420  seqomlem2  8426  oawordex  8530  oa00  8532  oaass  8534  om00  8548  odi  8552  omass  8553  oeordi  8561  oelim2  8569  omsmo  8632  eroveu  8798  eceqoveq  8808  map0g  8870  fundmen  9016  sdomdif  9101  onsdominel  9102  pssnn  9141  nneneq  9178  php3  9181  f1finf1o  9221  findcard3  9231  unblem1  9240  fiint  9274  ixpfi2  9295  dffi2  9371  elfiun  9378  fisup2g  9417  fiinf2g  9450  wemaplem2  9497  elirrv  9547  elirrvOLD  9548  preleqALT  9574  inf3lem2  9586  inf3lem3  9587  inf3lem6  9590  noinfep  9617  epfrs  9688  tcmin  9696  r1sdom  9734  tz9.12lem3  9749  rankelb  9784  bndrank  9801  rankunb  9810  rankuni2b  9813  cplem1  9863  karden  9869  carduni  9955  infxpenlem  9985  dfac8alem  10001  alephdom  10053  cardinfima  10069  alephval3  10082  dfac5lem4  10098  dfac5lem5  10099  dfac5  10100  dfac2b  10102  kmlem13  10134  nnadju  10169  ackbij1b  10209  cfub  10220  coflim  10233  cflim2  10235  cfslbn  10239  cfslb2n  10240  cofsmo  10241  cfsmolem  10242  sornom  10249  fincssdom  10295  isf32lem1  10325  isf32lem2  10326  isf32lem9  10333  isf34lem4  10349  isfin1-3  10358  axcc4  10411  domtriomlem  10414  axdc2lem  10420  axdc3lem2  10423  zorn2lem4  10471  zorn2lem6  10473  zornn0g  10477  uniimadom  10516  cardmin  10536  ficard  10537  konigthlem  10541  alephreg  10555  cfpwsdom  10557  axextnd  10564  fpwwe2lem5  10608  fpwwe2lem11  10614  fpwwe2lem12  10615  fpwwe2  10616  canthp1lem2  10626  gchpwdom  10643  winalim2  10669  tskuni  10756  grupr  10770  grur1a  10792  axgroth6  10801  grothomex  10802  eltskm  10816  addclpi  10865  nqereu  10902  ltexnq  10948  nsmallnq  10950  genpn0  10976  genpss  10977  genpnmax  10980  ltaddpr  11007  reclem3pr  11022  reclem4pr  11023  suplem1pr  11025  supsrlem  11084  1re  11196  dedekindle  11362  addrid  11378  negn0  11631  negf1o  11632  negfi  12155  sup2  12162  supadd  12174  supmullem1  12176  supmullem2  12177  zmulcl  12634  zeo  12673  uz11  12878  uzwo  12926  eqreznegel  12949  lbzbi  12951  qextlt  13220  qextle  13221  xrsupsslem  13324  xrinfmsslem  13325  supxrun  13333  supxrpnf  13335  supxrunb1  13336  supxrunb2  13337  fzm1  13626  uzrdgfni  13985  hasheqf1oi  14378  hashreshashfun  14466  leisorel  14487  fundmge2nop0  14529  wrdsymb0  14576  swrdnnn0nd  14684  swrdccatin2d  14771  cshinj  14838  repswcshw  14839  rennim  15280  01sqrexlem6  15288  caubnd  15400  sqreulem  15401  caucvgrlem  15714  fsumcvg  15753  supcvg  15900  prodeq2ii  15955  fprodcvg  15974  prodmo  15980  dvdslelem  16357  bitsinv1lem  16489  bitsshft  16523  smuval2  16530  smupvallem  16531  gcdcllem1  16547  bezoutlem2  16588  bezoutlem3  16589  algcvga  16627  isprm3  16731  isprm5  16756  oddprmdvds  16953  vdwlem13  17043  vdwnnlem1  17045  vdwnnlem3  17047  ramub1lem1  17076  prmgaplem5  17105  imasaddfnlem  17572  divsfval  17591  catpropd  17755  joindmss  18423  meetdmss  18437  psdmrn  18619  odlem1  19596  gexlem1  19640  cygctb  19953  rngisomring1  20541  lmodfopnelem1  20988  islss  21024  lspsneq0  21102  lspsneq  21215  psgnodpmr  21700  obselocv  21838  mvrf1  22095  evlseu  22194  mpfrcl  22196  ppttop  23125  epttop  23127  elcls  23191  restntr  23300  cnprest  23407  regsep  23452  nrmsep3  23473  lmmo  23498  cmpsublem  23517  cmpsub  23518  hauscmplem  23524  txcnpi  23726  txcnp  23738  fbun  23958  fbfinnfr  23959  trfbas2  23961  fgcl  23996  filssufilg  24029  ufinffr  24047  isfcls  24127  fclsrest  24142  flimfnfcls  24146  alexsubALTlem2  24166  alexsubALTlem3  24167  alexsubALTlem4  24168  alexsubALT  24169  cnextcn  24185  imasf1oxms  24607  metequiv2  24628  tngngpim  24777  iccpnfcnv  25064  iccpnfhmeo  25065  iscau2  25397  caun0  25401  minveclem3b  25548  itg1climres  25834  mbfi1fseqlem4  25838  ellimc3  25999  limccnp2  26012  dvlip  26113  itgsubstlem  26168  elply2  26314  coefv0  26366  coemulc  26373  ulmss  26518  sineq0  26647  scvxcvx  27108  sqf11  27261  ppiublem1  27324  fsumvma  27335  2sq2  27555  ostth  27761  ltsres  27784  nosepdmlem  27805  nobdaymin  27904  nocvxminlem  27905  addsprop  28127  mpteleeOLD  29154  brbtwn2  29164  colinearalg  29169  axcontlem4  29226  upgrres1  29572  usgr2trlncl  30018  umgrclwwlkge2  30251  upgr4cycl4dv4e  30445  1to3vfriendship  30541  3cyclfrgrrn1  30545  n4cyclfrgr  30551  frgrncvvdeqlem8  30566  frgrwopreg  30583  2clwwlk2clwwlk  30610  numclwwlk2lem1  30636  frgrreg  30654  frgrogt3nreg  30657  nmcvcn  30956  chlimi  31495  ocsh  31544  shsvs  31584  h1datomi  31842  stcl  32477  stge0  32485  stle1  32486  stm1addi  32506  stm1add3i  32508  cvnsym  32551  mdbr2  32557  dmdbr2  32564  mdsl0  32571  mdsl1i  32582  mdsl2i  32583  cvmdi  32585  atexch  32642  atcvat4i  32658  cdj1i  32694  1arithufdlem4  33754  xrge0iifcnv  34240  esumpr2  34374  sigaclci  34439  cntmeas  34533  mbfmcnt  34575  ballotlemfc0  34800  ballotlemfcc  34801  bnj1379  35135  bnj607  35221  bnj908  35236  bnj938  35242  bnj1174  35308  bnj1280  35325  f1resrcmplf1dlem  35390  fnrelpredd  35397  r1filimi  35411  fineqvinfep  35433  tz9.1regs  35442  axsepg2  35448  axsepg4  35451  axnulg  35453  axpowg2  35455  axpowg3  35456  cusgr3cyclex  35499  loop1cycl  35500  acycgrislfgr  35515  pthacycspth  35520  iccllysconn  35613  satffunlem1lem1  35765  satfvel  35775  sate0fv0  35780  antnestlaw2  36055  funpsstri  36129  fundmpss  36130  dfon2lem3  36146  dfon2lem4  36147  dfon2lem6  36149  dfon2lem9  36152  dfon2  36153  hbimtg  36167  hbaltg  36168  dfrdg4  36314  btwntriv2  36375  btwncomim  36376  btwnswapid  36380  btwnexch3  36383  ifscgr  36407  lineunray  36510  hilbert1.2  36518  cldbnd  36699  tailfb  36750  meran3  36786  arg-ax  36789  ontopbas  36801  onsuct0  36814  limsucncmpi  36818  ordcmp  36820  onint1  36822  weiunpo  36838  axtcond  36851  axuntco  36852  dfttc4lem2  36902  bj-bisimpl  37007  bj-bisimpr  37008  bj-syl66ib  37009  bj-gl4  37050  bj-alexim  37095  bj-nfimt  37107  bj-spvw  37119  bj-cbvalvv  37123  bj-ax6e  37152  bj-hbald  37166  axc11n11r  37170  bj-nnfim  37239  bj-nnfan  37241  bj-nnfor  37243  bj-nnford  37244  bj-19.21t  37248  bj-19.23t  37249  bj-19.42t  37252  bj-sbft  37265  bj-nnflemaa  37273  bj-nnflemae  37275  bj-hbsb3t  37285  bj-cbv2hv  37294  bj-equsal1t  37319  bj-axreprepsep  37572  bj-0int  37603  bj-bary1lem1  37815  topdifinffinlem  37853  isbasisrelowllem1  37861  isbasisrelowllem2  37862  iooelexlt  37868  finorwe  37888  finxpreclem1  37895  finxpreclem2  37896  isinf2  37911  fvineqsneu  37917  fvineqsneq  37918  pibt2  37923  wl-spae  38036  wl-19.8eqv  38038  wl-nfeqfb  38051  wl-mo3t  38091  wl-eujustlem1  38103  fin2so  38118  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  ismblfin  38172  indexdom  38245  fzmul  38252  heibor1lem  38320  heibor  38332  exidu1  38367  rngoideu  38414  zerdivemp1x  38458  ispridl2  38549  cnf1dd  38601  cnf2dd  38602  cnfn1dd  38603  cnfn2dd  38604  orcomdd  38678  disjlem14  39412  disjdmqsss  39416  disjdmqscossss  39417  prtlem14  39510  prter2  39517  aev-o  39567  ax12eq  39577  ax12el  39578  ax12indn  39579  ax12indi  39580  lsatn0  39635  lsatcmp  39639  lsatcv0  39667  lfl1dim  39757  lfl1dim2N  39758  lkrss2N  39805  lub0N  39825  glb0N  39829  glbconxN  40014  hl2at  40041  cvrexchlem  40055  cvratlem  40057  cvrat4  40079  psubspi  40383  pointpsubN  40387  elpaddn0  40436  paddasslem17  40472  ispsubcl2N  40583  ldilval  40749  trlord  41205  diaelrnN  41681  cdlemm10N  41754  cdlemn11pre  41846  dihord2pre  41861  dihglblem2N  41930  dihglblem3N  41931  mapdrvallem2  42281  ioin9i8  42836  sn-sup2  43125  incssnn0  43304  fphpd  43405  rmxycomplete  43506  dford3lem1  43615  iocinico  43801  onsupnmax  43817  cantnfresb  43913  cantnf2  43914  tfsconcatb0  43933  tfsconcat0b  43935  sdomne0  44001  sdomne0d  44002  ensucne0OLD  44118  al3im  44235  brtrclfv2  44315  frege129d  44351  frege60a  44466  frege60c  44511  frege70  44521  rfovcnvf1od  44592  clsk1indlem3  44631  neik0pk1imk0  44635  gneispace  44722  gneispaceel2  44732  gneispacess2  44734  dvconstbi  44908  axc5c4c711toc7  44978  axc5c4c711to11  44979  pm14.24  45006  sbiota1  45008  bi33imp12  45065  bi123imp0  45070  ee233  45093  vk15.4j  45102  ssralv2  45105  alrim3con13v  45107  tratrb  45110  onfrALTlem3  45118  onfrALTlem2  45120  19.41rg  45124  hbimpg  45128  hbalg  45129  ax6e2ndeq  45133  e2  45205  ee223  45208  sspwtrALT  45395  sspwtrALT2  45396  suctrALT2  45410  trintALT  45454  isosctrlem1ALT  45507  relpmin  45526  traxext  45551  modelaxreplem2  45553  ssclaxsep  45556  fnchoice  45607  mptfnd  45815  stoweidlem62  46634  2reu8i  47705  2reuimp  47707  ffnafv  47763  lswn0  48048  reupr  48126  reuopreuprim  48130  requad2  48243  bgoldbnnsum3prm  48424  bgoldbtbndlem2  48426  bgoldbtbndlem4  48428  gricsym  48541  gpgedgvtx1  48682  ply1mulgsumlem2  49018  iunord  50305  setrec2fun  50321