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

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  871  pm2.37  986  pm2.81  987  oplem1  1072  3jao  1453  impsingle  1660  al2im  1847  exlimdv  1968  19.23v  1977  spimfw  2000  ax13b  2067  nf5-1  2185  hbald  2208  19.8a  2221  spimedv  2237  19.9d  2243  sbequ1  2287  sbft  2307  cbv2w  2370  spimed  2420  cbv2  2435  cbv2h  2438  ax12  2455  axc11n  2458  equvini  2487  sb2  2511  sb4a  2512  mo3  2592  mopick  2653  moexexlem  2654  dvelimdc  2950  necon1ad  2976  necon4bd  2979  rsp2  3283  mo2icl  3675  2reu1  3849  reuss2  4274  reupick2  4279  elpwunsn  4645  sssn  4785  pwpw0  4834  iuneqconst  4966  disjiun  5094  trun  5226  reusv1  5363  reusv3i  5370  ralxfrALT  5381  exneq  5408  opth1  5448  copsexgwOLD  5465  copsexg  5466  opelopabt  5510  solin  5590  wefrc  5649  frinxp  5739  ssrelrn  5883  dmcosseq  5967  dmcosseqOLD  5968  reuop  6314  ordunidif  6431  oneqmini  6434  suctr  6469  ordsssuc2  6474  iotan0  6547  iotan0OLD  6548  fv3  6926  ndmfv  6940  ssimaex  6993  fvopab3ig  7012  iinpreima  7093  fvcofneq  7117  dff3  7124  dff4  7125  ffnfv  7143  fnsnr  7192  fprb  7222  elunirn  7278  f1mpt  7288  f1resrcmplf1dlem  7301  isomin  7368  oprabidw  7474  oprabid  7475  mpoeq123  7515  mpt3fvot2d  7714  sorpsscmpl  7774  dfwe2  7812  ssorduni  7817  ssonprc  7825  nlimsucg  7877  ordunisuc2  7879  tfinds  7895  ssnlim  7921  f1oweALT  8008  mptcnfimad  8022  el2mpocl  8122  f1o2ndf1  8160  frxp  8165  soxp  8168  poxp2  8187  poxp3  8194  poseq  8202  brtpos  8280  rntpos  8284  dftpos4  8290  onfununi  8377  onnseq  8380  smores2  8390  smo11  8400  tfr3  8435  rdglim2  8468  tz7.48lemOLD  8479  tz7.49  8483  seqomlem2  8489  oawordex  8593  oa00  8595  oaass  8597  om00  8611  odi  8615  omass  8616  oeordi  8624  oelim2  8632  omsmo  8695  eroveu  8861  eceqoveq  8871  map0g  8940  fundmen  9087  sdomdif  9172  onsdominel  9173  pssnn  9212  nneneq  9249  php3  9252  f1finf1o  9292  findcard3  9302  unblem1  9312  fiint  9346  ixpfi2  9367  dffi2  9442  elfiun  9449  fisup2g  9488  fiinf2g  9521  wemaplem2  9568  elirrv  9618  elirrvOLD  9619  preleqALT  9645  inf3lem2  9657  inf3lem3  9658  inf3lem6  9661  noinfep  9688  epfrs  9759  tcmin  9767  r1sdom  9808  tz9.12lem3  9823  rankelb  9860  bndrank  9881  rankunb  9891  rankuni2b  9894  r1filimi  9930  cplem1  9977  cplem1OLD  9978  kardenOLD  9987  setrec2fun  10000  carduni  10089  infxpenlem  10119  dfac8alem  10135  alephdom  10187  cardinfima  10203  alephval3  10216  dfac5lem4  10232  dfac5lem5  10233  dfac5  10234  dfac2b  10236  kmlem13  10268  nnadju  10303  ackbij1b  10343  cfub  10353  coflim  10366  cflim2  10368  cfslbn  10372  cfslb2n  10373  cofsmo  10374  cfsmolem  10375  sornom  10382  fincssdom  10428  isf32lem1  10458  isf32lem2  10459  isf32lem9  10466  isf34lem4  10482  isfin1-3  10491  axcc4  10544  domtriomlem  10547  axdc2lem  10553  axdc3lem2  10556  zorn2lem4  10604  zorn2lem6  10606  zornn0g  10610  uniimadom  10655  cardmin  10675  ficard  10676  konigthlem  10680  alephreg  10694  cfpwsdom  10696  axextnd  10703  fpwwe2lem5  10747  fpwwe2lem11  10753  fpwwe2lem12  10754  fpwwe2  10755  canthp1lem2  10765  gchpwdom  10782  winalim2  10808  tskuni  10895  grupr  10909  grur1a  10931  axgroth6  10940  grothomex  10941  eltskm  10955  addclpi  11004  nqereu  11041  ltexnq  11087  nsmallnq  11089  genpn0  11115  genpss  11116  genpnmax  11119  ltaddpr  11146  reclem3pr  11161  reclem4pr  11162  suplem1pr  11164  supsrlem  11223  1re  11335  dedekindle  11501  addrid  11517  negn0  11772  negf1o  11773  negfi  12293  sup2  12300  supadd  12312  supmullem1  12314  supmullem2  12315  zmulcl  12772  zeo  12812  uz11  13017  uzwo  13065  eqreznegel  13088  lbzbi  13090  qextlt  13360  qextle  13361  xrsupsslem  13464  xrinfmsslem  13465  supxrun  13473  supxrpnf  13475  supxrunb1  13476  supxrunb2  13477  fzm1  13768  uzrdgfni  14128  hasheqf1oi  14522  hashreshashfun  14611  leisorel  14632  fundmge2nop0  14674  wrdsymb0  14721  swrdnnn0nd  14834  swrdccatin2d  14921  cshinj  14990  repswcshw  14991  rennim  15435  01sqrexlem6  15443  caubnd  15555  sqreulem  15556  caucvgrlem  15869  fsumcvg  15907  supcvg  16054  prodeq2ii  16109  fprodcvg  16126  prodmo  16132  dvdslelem  16508  bitsinv1lem  16640  bitsshft  16674  smuval2  16681  smupvallem  16682  gcdcllem1  16698  bezoutlem2  16742  bezoutlem3  16743  algcvga  16783  isprm3  16887  isprm5  16912  oddprmdvds  17110  vdwlem13  17200  vdwnnlem1  17202  vdwnnlem3  17204  ramub1lem1  17233  prmgaplem5  17262  imasaddfnlem  17729  divsfval  17748  catpropd  17912  joindmss  18580  meetdmss  18594  psdmrn  18776  odlem1  19779  gexlem1  19823  cygctb  20136  rngisomring1  20728  lmodfopnelem1  21203  islss  21239  lspsneq0  21317  lspsneq  21430  psgnodpmr  21926  obselocv  22064  mvrf1  22323  evlseu  22422  mpfrcl  22424  ppttop  23355  epttop  23357  elcls  23421  restntr  23530  cnprest  23637  regsep  23682  nrmsep3  23703  lmmo  23728  cmpsublem  23747  cmpsub  23748  hauscmplem  23754  txcnpi  23957  txcnp  23969  fbun  24189  fbfinnfr  24190  trfbas2  24192  fgcl  24227  filssufilg  24260  ufinffr  24278  isfcls  24358  fclsrest  24373  flimfnfcls  24377  alexsubALTlem2  24397  alexsubALTlem3  24398  alexsubALTlem4  24399  alexsubALT  24400  cnextcn  24416  imasf1oxms  24838  metequiv2  24859  tngngpim  25008  iccpnfcnv  25295  iccpnfhmeo  25296  iscau2  25628  caun0  25632  minveclem3b  25779  itg1climres  26065  mbfi1fseqlem4  26069  ellimc3  26229  limccnp2  26242  dvlip  26343  itgsubstlem  26398  elply2  26544  coefv0  26597  coemulc  26604  ulmss  26754  sineq0  26882  scvxcvx  27343  sqf11  27496  ppiublem1  27559  fsumvma  27570  2sq2  27790  ostth  27996  ltsres  28049  nosepdmlem  28070  nobdaymin  28169  nocvxminlem  28170  addsprop  28392  mpteleeOLD  29503  brbtwn2  29513  colinearalg  29518  axcontlem4  29575  upgrres1  29924  usgr2trlncl  30376  umgrclwwlkge2  30612  loop1cycl  30774  upgr4cycl4dv4e  30816  1to3vfriendship  30912  3cyclfrgrrn1  30916  n4cyclfrgr  30922  frgrncvvdeqlem8  30937  frgrwopreg  30954  2clwwlk2clwwlk  30981  numclwwlk2lem1  31007  frgrreg  31025  frgrogt3nreg  31028  nmcvcn  31327  chlimi  31866  ocsh  31915  shsvs  31955  h1datomi  32213  stcl  32848  stge0  32856  stle1  32857  stm1addi  32877  stm1add3i  32879  cvnsym  32922  mdbr2  32928  dmdbr2  32935  mdsl0  32942  mdsl1i  32953  mdsl2i  32954  cvmdi  32956  atexch  33013  atcvat4i  33029  cdj1i  33065  1arithufdlem4  34149  xrge0iifcnv  34635  esumpr2  34769  sigaclci  34834  cntmeas  34929  mbfmcnt  34970  ballotlemfc0  35195  ballotlemfcc  35196  bnj1379  35530  bnj607  35616  bnj908  35631  bnj938  35637  bnj1174  35703  bnj1280  35720  ordunmax  35792  mpofvop2d  35799  soinfdom  35800  fnrelpredd  35804  fineqvinfep  35893  tz9.1regs  35902  axsepg2  35908  axsepg4  35911  axnulg  35913  axpowg2  35915  axpowg3  35916  kardcard2b  35933  ackardcard  35935  j0ltaleph  36008  cusgr3cyclex  36068  acycgrislfgr  36074  pthacycspth  36079  iccllysconn  36182  satffunlem1lem1  36334  satfvel  36344  sate0fv0  36349  antnestlaw2  36624  elpssmo  36636  funpsstri  36709  fundmpss  36710  dfon2lem3  36725  dfon2lem4  36726  dfon2lem6  36728  dfon2lem9  36731  dfon2  36732  hbimtg  36746  hbaltg  36747  dfrdg4  36893  btwntriv2  36955  btwncomim  36956  btwnswapid  36960  btwnexch3  36963  ifscgr  36987  lineunray  37090  hilbert1.2  37098  cldbnd  37292  tailfb  37343  meran3  37379  arg-ax  37382  ontopbas  37394  onsuct0  37407  limsucncmpi  37411  ordcmp  37413  onint1  37415  weiunpo  37431  axtcond  37444  axuntco  37445  dfttc4lem2  37495  bj-bisimpl  37600  bj-bisimpr  37601  bj-syl66ib  37602  bj-gl4  37643  bj-alexim  37688  bj-nfimt  37700  bj-spvw  37712  bj-cbvalvv  37716  bj-ax6e  37745  bj-hbald  37759  axc11n11r  37763  bj-nnfim  37832  bj-nnfan  37834  bj-nnfor  37836  bj-nnford  37837  bj-19.21t  37841  bj-19.23t  37842  bj-19.42t  37845  bj-sbft  37858  bj-nnflemaa  37866  bj-nnflemae  37868  bj-hbsb3t  37878  bj-cbv2hv  37887  bj-equsal1t  37912  bj-axreprepsep  38182  bj-0int  38213  bj-bary1lem1  38424  topdifinffinlem  38462  isbasisrelowllem1  38470  isbasisrelowllem2  38471  iooelexlt  38477  finorwe  38497  finxpreclem1  38504  finxpreclem2  38505  isinf2  38520  fvineqsneu  38526  fvineqsneq  38527  pibt2  38532  wl-spae  38645  wl-19.8eqv  38647  wl-nfeqfb  38660  wl-mo3t  38700  wl-eujustlem1  38712  fin2so  38722  poimirlem29  38759  poimirlem30  38760  poimirlem31  38761  poimirlem32  38762  ismblfin  38771  indexdom  38860  fzmul  38867  heibor1lem  38935  heibor  38947  exidu1  38982  rngoideu  39029  zerdivemp1x  39073  ispridl2  39164  cnf1dd  39214  cnf2dd  39215  cnfn1dd  39216  cnfn2dd  39217  orcomdd  39291  disjlem14  40025  disjdmqsss  40029  disjdmqscossss  40030  prtlem14  40123  prter2  40130  aev-o  40180  ax12eq  40190  ax12el  40191  ax12indn  40192  ax12indi  40193  lsatn0  40248  lsatcmp  40252  lsatcv0  40280  lfl1dim  40370  lfl1dim2N  40371  lkrss2N  40418  lub0N  40438  glb0N  40442  glbconxN  40627  hl2at  40654  cvrexchlem  40668  cvratlem  40670  cvrat4  40692  psubspi  40996  pointpsubN  41000  elpaddn0  41049  paddasslem17  41085  ispsubcl2N  41196  ldilval  41362  trlord  41818  diaelrnN  42294  cdlemm10N  42367  cdlemn11pre  42459  dihord2pre  42474  dihglblem2N  42543  dihglblem3N  42544  mapdrvallem2  42894  ioin9i8  43451  sn-sup2  43748  incssnn0  43915  fphpd  44016  rmxycomplete  44117  dford3lem1  44226  iocinico  44406  onsupnmax  44422  cantnfresb  44518  cantnf2  44519  tfsconcatb0  44538  tfsconcat0b  44540  sdomne0  44606  sdomne0d  44607  ensucne0OLD  44723  al3im  44839  brtrclfv2  44919  frege129d  44955  frege60a  45070  frege60c  45115  frege70  45125  rfovcnvf1od  45196  clsk1indlem3  45235  neik0pk1imk0  45239  gneispace  45326  gneispaceel2  45336  gneispacess2  45338  dvconstbi  45510  axc5c4c711toc7  45580  axc5c4c711to11  45581  pm14.24  45607  sbiota1  45609  bi33imp12  45665  bi123imp0  45670  ee233  45693  vk15.4j  45702  ssralv2  45705  alrim3con13v  45707  tratrb  45710  onfrALTlem3  45718  onfrALTlem2  45720  19.41rg  45724  hbimpg  45728  hbalg  45729  ax6e2ndeq  45733  e2  45805  ee223  45808  sspwtrALT  45995  sspwtrALT2  45996  suctrALT2  46010  trintALT  46054  isosctrlem1ALT  46107  dmstructnn  46119  dmstructfi  46120  relpmin  46137  traxext  46162  modelaxreplem2  46164  ssclaxsep  46167  fnchoice  46251  mptfnd  46459  stoweidlem62  47277  2reu8i  48389  2reuimp  48391  ffnafv  48446  lswn0  48731  reupr  48809  reuopreuprim  48813  requad2  48926  bgoldbnnsum3prm  49107  bgoldbtbndlem2  49109  bgoldbtbndlem4  49111  gricsym  49224  gpgedgvtx1  49365  ply1mulgsumlem2  49704  iunord  51064