Theorem syl6 34

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  35  syl6com  36  a1dd  48  syl6mpi  65  syl6c  68  syl10  77  com34  89  con1d  138  expi  160  looinv  193  syl6ib  240  syl6ibr  241  syl6bi  242  syl6bir  243  jaoi  393  syl6an  566  pm2.37  885  pm2.81  892  oplem1  999  3jao  1381  al2im  1732  nfimd  1812  exlimdv  1848  spimfw  1865  ax13b  1951  nf5-1  2010  hbald  2028  19.9d  2058  19.9ht  2128  spimed  2243  cbv2h  2257  axc15  2291  ax12  2292  axc11n  2295  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  ax12v2OLD  2330  equvini  2334  hbsb2  2347  dfsb2  2361  sbequi  2363  sbft  2367  sbi1  2380  mo3  2495  mopick  2523  moexex  2529  dvelimdc  2772  necon1ad  2799  necon4bd  2802  rsp2  2920  mo2icl  3352  reuss2  3866  reupick2  3872  elpwunsn  4171  pwpw0  4284  sssn  4298  pwsnALT  4367  dfiun2g  4488  disjiun  4573  axsep  4708  reusv1  4792  reusv3i  4801  ralxfrALT  4813  opth1  4870  copsexg  4882  opelopabt  4912  wefrc  5032  frinxp  5107  ssrelrn  5237  issref  5428  ordunidif  5690  oneqmini  5693  suctr  5725  suctrOLD  5726  ordsssuc2  5731  iotaval  5779  fv3  6116  ndmfv  6128  ssimaex  6173  fvopab3ig  6188  iinpreima  6253  fvcofneq  6275  dff3  6280  dff4  6281  ffnfv  6295  fnsnb  6337  elunirn  6413  f1mpt  6419  isomin  6487  oprabid  6576  mpt2eq123  6612  sorpsscmpl  6846  dfwe2  6873  ssorduni  6877  ssonprc  6884  nlimsucg  6934  ordunisuc2  6936  tfinds  6951  ssnlim  6975  fun11iun  7019  f1oweALT  7043  el2mpt2cl  7138  f1o2ndf1  7172  frxp  7174  soxp  7177  brtpos  7248  rntpos  7252  dftpos4  7258  onfununi  7325  onnseq  7328  smores2  7338  smo11  7348  tfr3  7382  rdglim2  7415  tz7.48lem  7423  tz7.49  7427  seqomlem2  7433  oawordex  7524  oa00  7526  oaass  7528  om00  7542  odi  7546  omass  7547  oeordi  7554  oelim2  7562  omsmo  7621  eroveu  7729  eceqoveq  7740  map0g  7783  fundmen  7916  sdomdif  7993  onsdominel  7994  nneneq  8028  php3  8031  onomeneq  8035  pssnn  8063  f1finf1o  8072  findcard3  8088  unblem1  8097  fiint  8122  ixpfi2  8147  dffi2  8212  elfiun  8219  fisup2g  8257  fiinf2g  8289  wemaplem2  8335  preleq  8397  inf3lem2  8409  inf3lem3  8410  inf3lem6  8413  noinfep  8440  epfrs  8490  tcmin  8500  r1sdom  8520  r1ord3g  8525  r1ord2  8527  tz9.12lem3  8535  rankelb  8570  bndrank  8587  rankunb  8596  rankuni2b  8599  cplem1  8635  karden  8641  carduni  8690  infxpenlem  8719  dfac8alem  8735  alephdom  8787  cardinfima  8803  alephval3  8816  dfac5lem4  8832  dfac5lem5  8833  dfac5  8834  dfac2  8836  kmlem13  8867  ackbij1b  8944  cfub  8954  coflim  8966  cflim2  8968  cfslbn  8972  cfslb2n  8973  cofsmo  8974  cfsmolem  8975  sornom  8982  fincssdom  9028  isf32lem1  9058  isf32lem2  9059  isf32lem9  9066  isf34lem4  9082  isfin1-3  9091  axcc4  9144  domtriomlem  9147  axdc2lem  9153  axdc3lem2  9156  zorn2lem4  9204  zorn2lem6  9206  zornn0g  9210  axdclem2  9225  uniimadom  9245  cardmin  9265  ficard  9266  konigthlem  9269  alephreg  9283  cfpwsdom  9285  axextnd  9292  fpwwe2lem6  9336  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  canthp1lem2  9354  winalim2  9397  tskuni  9484  grupr  9498  grur1a  9520  axgroth6  9529  grothomex  9530  eltskm  9544  addclpi  9593  nqereu  9630  ltexnq  9676  nsmallnq  9678  genpn0  9704  genpss  9705  genpnmax  9708  ltaddpr  9735  reclem3pr  9750  reclem4pr  9751  suplem1pr  9753  supsrlem  9811  1re  9918  dedekindle  10080  addid1  10095  negn0  10338  negf1o  10339  negfi  10850  fiminre  10851  sup2  10858  supadd  10868  supmullem1  10870  supmullem2  10871  zmulcl  11303  zeo  11339  uz11  11586  uzwo  11627  eqreznegel  11650  lbzbi  11652  qextlt  11908  qextle  11909  xrsupsslem  12009  xrinfmsslem  12010  supxrun  12018  supxrpnf  12020  supxrunb1  12021  supxrunb2  12022  fzm1  12289  uzrdgfni  12619  hasheqf1oi  13002  hasheqf1oiOLD  13003  leisorel  13101  wrdsymb0  13194  swrdccatin2d  13351  cshinj  13408  repswcshw  13409  rennim  13827  sqrlem6  13836  caubnd  13946  sqreulem  13947  rlimclim  14125  caucvgrlem  14251  fsumcvg  14290  supcvg  14427  prodeq2ii  14482  fprodcvg  14499  prodmo  14505  dvdslelem  14869  bitsinv1lem  15001  bitsshft  15035  smuval2  15042  smupvallem  15043  gcdcllem1  15059  bezoutlem2  15095  bezoutlem3  15096  algcvga  15130  isprm3  15234  isprm5  15257  oddprmdvds  15445  vdwlem13  15535  vdwnnlem1  15537  vdwnnlem3  15539  ramub1lem1  15568  prmgaplem5  15597  imasaddfnlem  16011  divsfval  16030  catpropd  16192  joindmss  16830  meetdmss  16844  psdmrn  17030  odlem1  17777  gexlem1  17817  cygctb  18116  lmodfopnelem1  18722  islss  18756  lspsneq0  18833  lspsneq  18943  mvrf1  19246  evlseu  19337  mpfrcl  19339  psgnodpmr  19755  obselocv  19891  ppttop  20621  epttop  20623  elcls  20687  restntr  20796  cnprest  20903  regsep  20948  nrmsep3  20969  lmmo  20994  cmpsublem  21012  cmpsub  21013  hauscmplem  21019  txcnpi  21221  txcnp  21233  fbun  21454  fbfinnfr  21455  trfbas2  21457  fgcl  21492  filssufilg  21525  ufinffr  21543  isfcls  21623  fclsrest  21638  flimfnfcls  21642  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  cnextcn  21681  imasf1oxms  22104  metequiv2  22125  tngngpim  22273  iccpnfcnv  22551  iccpnfhmeo  22552  iscau2  22883  caun0  22887  minveclem3b  23007  itg1climres  23287  mbfi1fseqlem4  23291  ellimc3  23449  limccnp2  23462  dvlip  23560  itgsubstlem  23615  elply2  23756  coefv0  23808  coemulc  23815  ulmss  23955  sineq0  24077  scvxcvx  24512  sqf11  24665  ppiublem1  24727  fsumvma  24738  ostth  25128  mptelee  25575  brbtwn2  25585  colinearalg  25590  axcontlem4  25647  usgrafisinds  25942  nbgra0nb  25958  nbgraf1olem5  25974  cusgrafi  26010  spthispth  26103  wlkdvspthlem  26137  usgra2adedgwlkon  26143  usgra2adedgwlkonALT  26144  4cycl4dv  26195  clwlkfclwwlk  26371  nbhashuvtx1  26442  1to3vfriendship  26535  3cyclfrgrarn1  26539  n4cyclfrgra  26545  frgrancvvdeqlemB  26565  frg2wot1  26584  frg2woteq  26587  numclwwlkovf2ex  26613  numclwwlk2lem1  26629  frgraogt3nreg  26647  nmcvcn  26934  chlimi  27475  ocsh  27526  shsvs  27566  h1datomi  27824  stcl  28459  stge0  28467  stle1  28468  stm1addi  28488  stm1add3i  28490  cvnsym  28533  mdbr2  28539  dmdbr2  28546  mdsl0  28553  mdsl1i  28564  mdsl2i  28565  cvmdi  28567  atexch  28624  atcvat4i  28640  cdj1i  28676  xrge0iifcnv  29307  esumpr2  29456  sigaclci  29522  cntmeas  29616  mbfmcnt  29657  ballotlemfc0  29881  ballotlemfcc  29882  bnj142OLD  30048  bnj1379  30155  bnj607  30240  bnj908  30255  bnj938  30261  bnj1174  30325  bnj1280  30342  iccllyscon  30486  funpsstri  30909  fundmpss  30910  fprb  30916  dfon2lem3  30934  dfon2lem4  30935  dfon2lem6  30937  dfon2lem9  30940  dfon2  30941  hbimtg  30956  hbaltg  30957  dftrpred3g  30977  poseq  30994  frrlem5b  31029  frrlem5d  31031  sltres  31061  nocvxminlem  31089  nocvxmin  31090  nofulllem5  31105  dfrdg4  31228  btwntriv2  31289  btwncomim  31290  btwnswapid  31294  btwnexch3  31297  ifscgr  31321  lineunray  31424  hilbert1.2  31432  cldbnd  31491  tailfb  31542  meran3  31582  arg-ax  31585  ontopbas  31597  onsuct0  31610  limsucncmpi  31614  ordcmp  31616  onint1  31618  bj-gl4  31753  bj-alrimhi  31789  bj-nalnalimiOLD  31799  bj-ax6e  31842  bj-hbalt  31858  axc11n11r  31860  bj-hbsb3t  31899  bj-spimedv  31906  bj-cbv2hv  31918  bj-sbftv  31951  bj-axsep  31981  bj-equsal1t  31997  bj-mo3OLD  32022  bj-syl66ib  32023  bj-bary1lem1  32338  topdifinffinlem  32371  isbasisrelowllem1  32379  isbasisrelowllem2  32380  iooelexlt  32386  finxpreclem1  32402  finxpreclem2  32403  wl-nf-nf2  32463  wl-spae  32485  wl-19.8eqv  32488  wl-nfeqfb  32502  wl-lem-moexsb  32529  wl-mo3t  32537  wl-ax11-lem3  32543  fin2so  32566  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  ismblfin  32620  indexdom  32699  fzmul  32707  heibor1lem  32778  heibor  32790  exidu1  32825  rngoideu  32872  zerdivemp1x  32916  ispridl2  33007  orcomdd  33061  cnf1dd  33062  cnfn1dd  33064  cnfn2dd  33065  prtlem14  33177  prter2  33184  aev-o  33234  ax12eq  33244  ax12el  33245  ax12indn  33246  ax12indi  33247  lsatn0  33304  lsatcmp  33308  lsatcv0  33336  lfl1dim  33426  lfl1dim2N  33427  lkrss2N  33474  lub0N  33494  glb0N  33498  glbconxN  33682  hl2at  33709  cvrexchlem  33723  cvratlem  33725  cvrat4  33747  psubspi  34051  pointpsubN  34055  elpaddn0  34104  paddasslem17  34140  ispsubcl2N  34251  ldilval  34417  trlord  34875  diaelrnN  35352  cdlemm10N  35425  cdlemn11pre  35517  dihord2pre  35532  dihglblem2N  35601  dihglblem3N  35602  mapdrvallem2  35952  incssnn0  36292  fphpd  36398  rmxycomplete  36500  dford3lem1  36611  iocinico  36816  al3im  36957  brtrclfv2  37038  frege129d  37074  frege60a  37192  frege60c  37237  frege70  37247  rfovcnvf1od  37318  clsk1indlem3  37361  neik0pk1imk0  37365  gneispace  37452  gneispaceel2  37462  gneispacess2  37464  dvconstbi  37555  axc5c4c711toc7  37627  axc5c4c711to11  37628  pm14.24  37655  sbiota1  37657  bi33imp12  37717  bi123imp0  37723  ee233  37746  vk15.4j  37755  ssralv2  37758  alrim3con13v  37764  tratrb  37767  onfrALTlem3  37780  onfrALTlem2  37782  19.41rg  37787  hbimpg  37791  hbalg  37792  ax6e2ndeq  37796  e2  37877  ee223  37880  sspwtrALT  38071  sspwtrALT2  38080  suctrALT2  38094  trintALT  38139  isosctrlem1ALT  38192  fnchoice  38211  stoweidlem62  38955  2reu1  39835  ffnafv  39900  bgoldbnnsum3prm  40220  bgoldbtbndlem2  40222  bgoldbtbndlem4  40224  lswn0  40242  upgrres1  40532  upgrwlkdvde  40943  usgr2trlncl  40966  umgrclwwlksge2  41219  clwlksfclwwlk  41269  clwwlksnun  41281  upgr4cycl4dv4e  41352  1to3vfriendship-av  41451  3cyclfrgrrn1  41455  n4cyclfrgr  41461  frgrncvvdeqlemB  41477  frgr2wwlk1  41494  av-numclwwlkovf2ex  41517  av-numclwwlk2lem1  41532  av-frgrareg  41548  av-frgraogt3nreg  41551  ply1mulgsumlem2  41969  iunord  42220  setrec2fun  42238