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  2917  necon1ad  2943  necon4bd  2946  rsp2  3255  mo2icl  3688  2reu1  3863  reuss2  4292  reupick2  4297  elpwunsn  4651  pwpw0  4780  sssn  4793  iuneqconst  4970  disjiun  5098  reusv1  5355  reusv3i  5362  ralxfrALT  5373  exneq  5398  opth1  5438  copsexgw  5453  copsexg  5454  opelopabt  5495  solin  5576  wefrc  5635  frinxp  5724  ssrelrn  5861  dmcosseq  5943  reuop  6269  ordunidif  6385  oneqmini  6388  suctr  6423  ordsssuc2  6428  iotan0  6504  fv3  6879  ndmfv  6896  ssimaex  6949  fvopab3ig  6967  iinpreima  7044  fvcofneq  7068  dff3  7075  dff4  7076  ffnfv  7094  fnsnr  7140  fprb  7171  elunirn  7228  f1mpt  7239  isomin  7315  oprabidw  7421  oprabid  7422  mpoeq123  7464  sorpsscmpl  7713  dfwe2  7753  ssorduni  7758  ssonprc  7766  nlimsucg  7821  ordunisuc2  7823  tfinds  7839  ssnlim  7865  f1oweALT  7954  mptcnfimad  7968  el2mpocl  8068  f1o2ndf1  8104  frxp  8108  soxp  8111  poxp2  8125  poxp3  8132  poseq  8140  brtpos  8217  rntpos  8221  dftpos4  8227  onfununi  8313  onnseq  8316  smores2  8326  smo11  8336  tfr3  8370  rdglim2  8403  tz7.48lem  8412  tz7.49  8416  seqomlem2  8422  oawordex  8524  oa00  8526  oaass  8528  om00  8542  odi  8546  omass  8547  oeordi  8554  oelim2  8562  omsmo  8625  eroveu  8788  eceqoveq  8798  map0g  8860  fundmen  9005  sdomdif  9095  onsdominel  9096  pssnn  9138  nneneq  9176  php3  9179  f1finf1o  9223  f1finf1oOLD  9224  findcard3  9236  findcard3OLD  9237  unblem1  9246  fiint  9284  fiintOLD  9285  ixpfi2  9308  dffi2  9381  elfiun  9388  fisup2g  9427  fiinf2g  9460  wemaplem2  9507  preleqALT  9577  inf3lem2  9589  inf3lem3  9590  inf3lem6  9593  noinfep  9620  epfrs  9691  tcmin  9701  r1sdom  9734  tz9.12lem3  9749  rankelb  9784  bndrank  9801  rankunb  9810  rankuni2b  9813  cplem1  9849  karden  9855  carduni  9941  infxpenlem  9973  dfac8alem  9989  alephdom  10041  cardinfima  10057  alephval3  10070  dfac5lem4  10086  dfac5lem5  10087  dfac5lem4OLD  10088  dfac5  10089  dfac2b  10091  kmlem13  10123  nnadju  10158  ackbij1b  10198  cfub  10209  coflim  10221  cflim2  10223  cfslbn  10227  cfslb2n  10228  cofsmo  10229  cfsmolem  10230  sornom  10237  fincssdom  10283  isf32lem1  10313  isf32lem2  10314  isf32lem9  10321  isf34lem4  10337  isfin1-3  10346  axcc4  10399  domtriomlem  10402  axdc2lem  10408  axdc3lem2  10411  zorn2lem4  10459  zorn2lem6  10461  zornn0g  10465  uniimadom  10504  cardmin  10524  ficard  10525  konigthlem  10528  alephreg  10542  cfpwsdom  10544  axextnd  10551  fpwwe2lem5  10595  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  canthp1lem2  10613  gchpwdom  10630  winalim2  10656  tskuni  10743  grupr  10757  grur1a  10779  axgroth6  10788  grothomex  10789  eltskm  10803  addclpi  10852  nqereu  10889  ltexnq  10935  nsmallnq  10937  genpn0  10963  genpss  10964  genpnmax  10967  ltaddpr  10994  reclem3pr  11009  reclem4pr  11010  suplem1pr  11012  supsrlem  11071  1re  11181  dedekindle  11345  addrid  11361  negn0  11614  negf1o  11615  negfi  12139  sup2  12146  supadd  12158  supmullem1  12160  supmullem2  12161  zmulcl  12589  zeo  12627  uz11  12825  uzwo  12877  eqreznegel  12900  lbzbi  12902  qextlt  13170  qextle  13171  xrsupsslem  13274  xrinfmsslem  13275  supxrun  13283  supxrpnf  13285  supxrunb1  13286  supxrunb2  13287  fzm1  13575  uzrdgfni  13930  hasheqf1oi  14323  hashreshashfun  14411  leisorel  14432  fundmge2nop0  14474  wrdsymb0  14521  swrdnnn0nd  14628  swrdccatin2d  14716  cshinj  14783  repswcshw  14784  rennim  15212  01sqrexlem6  15220  caubnd  15332  sqreulem  15333  caucvgrlem  15646  fsumcvg  15685  supcvg  15829  prodeq2ii  15884  fprodcvg  15903  prodmo  15909  dvdslelem  16286  bitsinv1lem  16418  bitsshft  16452  smuval2  16459  smupvallem  16460  gcdcllem1  16476  bezoutlem2  16517  bezoutlem3  16518  algcvga  16556  isprm3  16660  isprm5  16684  oddprmdvds  16881  vdwlem13  16971  vdwnnlem1  16973  vdwnnlem3  16975  ramub1lem1  17004  prmgaplem5  17033  imasaddfnlem  17498  divsfval  17517  catpropd  17677  joindmss  18345  meetdmss  18359  psdmrn  18539  odlem1  19472  gexlem1  19516  cygctb  19829  rngisomring1  20384  lmodfopnelem1  20811  islss  20847  lspsneq0  20925  lspsneq  21039  psgnodpmr  21506  obselocv  21644  mvrf1  21902  evlseu  21997  mpfrcl  21999  ppttop  22901  epttop  22903  elcls  22967  restntr  23076  cnprest  23183  regsep  23228  nrmsep3  23249  lmmo  23274  cmpsublem  23293  cmpsub  23294  hauscmplem  23300  txcnpi  23502  txcnp  23514  fbun  23734  fbfinnfr  23735  trfbas2  23737  fgcl  23772  filssufilg  23805  ufinffr  23823  isfcls  23903  fclsrest  23918  flimfnfcls  23922  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  cnextcn  23961  imasf1oxms  24384  metequiv2  24405  tngngpim  24554  iccpnfcnv  24849  iccpnfhmeo  24850  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  33525  xrge0iifcnv  33930  esumpr2  34064  sigaclci  34129  cntmeas  34223  mbfmcnt  34266  ballotlemfc0  34491  ballotlemfcc  34492  bnj1379  34827  bnj607  34913  bnj908  34928  bnj938  34934  bnj1174  35000  bnj1280  35017  f1resrcmplf1dlem  35083  fnrelpredd  35086  axnulg  35089  cusgr3cyclex  35130  loop1cycl  35131  acycgrislfgr  35146  pthacycspth  35151  iccllysconn  35244  satffunlem1lem1  35396  satfvel  35406  sate0fv0  35411  antnestlaw2  35686  funpsstri  35760  fundmpss  35761  dfon2lem3  35780  dfon2lem4  35781  dfon2lem6  35783  dfon2lem9  35786  dfon2  35787  hbimtg  35801  hbaltg  35802  dfrdg4  35946  btwntriv2  36007  btwncomim  36008  btwnswapid  36012  btwnexch3  36015  ifscgr  36039  lineunray  36142  hilbert1.2  36150  cldbnd  36321  tailfb  36372  meran3  36408  arg-ax  36411  ontopbas  36423  onsuct0  36436  limsucncmpi  36440  ordcmp  36442  onint1  36444  weiunpo  36460  bj-syl66ib  36550  bj-gl4  36590  bj-alexim  36622  bj-nfimt  36633  bj-ax6e  36663  bj-hbalt  36676  axc11n11r  36678  bj-nnfim  36741  bj-nnfan  36743  bj-nnfor  36745  bj-nnford  36746  bj-nnflemaa  36757  bj-nnflemae  36759  bj-19.21t  36764  bj-19.23t  36765  bj-19.42t  36768  bj-sbft  36770  bj-hbsb3t  36783  bj-cbv2hv  36792  bj-equsal1t  36817  bj-0int  37096  bj-bary1lem1  37306  topdifinffinlem  37342  isbasisrelowllem1  37350  isbasisrelowllem2  37351  iooelexlt  37357  finorwe  37377  finxpreclem1  37384  finxpreclem2  37385  isinf2  37400  fvineqsneu  37406  fvineqsneq  37407  pibt2  37412  wl-spae  37516  wl-19.8eqv  37518  wl-nfeqfb  37531  wl-mo3t  37571  wl-ax11-lem3  37582  fin2so  37608  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  ismblfin  37662  indexdom  37735  fzmul  37742  heibor1lem  37810  heibor  37822  exidu1  37857  rngoideu  37904  zerdivemp1x  37948  ispridl2  38039  cnf1dd  38091  cnf2dd  38092  cnfn1dd  38093  cnfn2dd  38094  orcomdd  38168  disjlem14  38797  disjdmqsss  38801  disjdmqscossss  38802  prtlem14  38874  prter2  38881  aev-o  38931  ax12eq  38941  ax12el  38942  ax12indn  38943  ax12indi  38944  lsatn0  38999  lsatcmp  39003  lsatcv0  39031  lfl1dim  39121  lfl1dim2N  39122  lkrss2N  39169  lub0N  39189  glb0N  39193  glbconxN  39379  hl2at  39406  cvrexchlem  39420  cvratlem  39422  cvrat4  39444  psubspi  39748  pointpsubN  39752  elpaddn0  39801  paddasslem17  39837  ispsubcl2N  39948  ldilval  40114  trlord  40570  diaelrnN  41046  cdlemm10N  41119  cdlemn11pre  41211  dihord2pre  41226  dihglblem2N  41295  dihglblem3N  41296  mapdrvallem2  41646  ioin9i8  42202  sn-sup2  42486  incssnn0  42706  fphpd  42811  rmxycomplete  42913  dford3lem1  43022  iocinico  43208  onsupnmax  43224  cantnfresb  43320  cantnf2  43321  tfsconcatb0  43340  tfsconcat0b  43342  sdomne0  43409  sdomne0d  43410  ensucne0OLD  43526  al3im  43643  brtrclfv2  43723  frege129d  43759  frege60a  43874  frege60c  43919  frege70  43929  rfovcnvf1od  44000  clsk1indlem3  44039  neik0pk1imk0  44043  gneispace  44130  gneispaceel2  44140  gneispacess2  44142  dvconstbi  44330  axc5c4c711toc7  44400  axc5c4c711to11  44401  pm14.24  44428  sbiota1  44430  bi33imp12  44488  bi123imp0  44493  ee233  44516  vk15.4j  44525  ssralv2  44528  alrim3con13v  44530  tratrb  44533  onfrALTlem3  44541  onfrALTlem2  44543  19.41rg  44547  hbimpg  44551  hbalg  44552  ax6e2ndeq  44556  e2  44628  ee223  44631  sspwtrALT  44818  sspwtrALT2  44819  suctrALT2  44833  trintALT  44877  isosctrlem1ALT  44930  relpmin  44949  traxext  44974  modelaxreplem2  44976  ssclaxsep  44979  fnchoice  45030  mptfnd  45243  stoweidlem62  46067  2reu8i  47118  2reuimp  47120  ffnafv  47176  lswn0  47449  reupr  47527  reuopreuprim  47531  requad2  47628  bgoldbnnsum3prm  47809  bgoldbtbndlem2  47811  bgoldbtbndlem4  47813  gricsym  47925  gpgedgvtx1  48057  ply1mulgsumlem2  48380  iunord  49669  setrec2fun  49685