MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anc2 Structured version   Visualization version   GIF version

Theorem syl2anc2 585
Description: Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.)
Hypotheses
Ref Expression
syl2anc2.1 (𝜑𝜓)
syl2anc2.2 (𝜓𝜒)
syl2anc2.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2anc2 (𝜑𝜃)

Proof of Theorem syl2anc2
StepHypRef Expression
1 syl2anc2.1 . 2 (𝜑𝜓)
2 syl2anc2.2 . . 3 (𝜓𝜒)
31, 2syl 17 . 2 (𝜑𝜒)
4 syl2anc2.3 . 2 ((𝜓𝜒) → 𝜃)
51, 3, 4syl2anc 584 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 397
This theorem is referenced by:  ssnnfiOLD  9111  php4  9154  djulepw  10125  infdjuabs  10139  xrsupss  13225  xrinfmss  13226  trclfv  14882  isumsplit  15722  ram0  16891  0mhm  18627  grpidssd  18819  gexdvds  19362  lsmdisj2  19460  mulgnn0di  19600  odadd1  19622  gsumval3  19680  telgsums  19766  dprdfadd  19795  ringlz  20007  ringrz  20008  lspsneq  20579  dsmmacl  21143  mplsubglem  21401  scmatmhm  21879  mdetuni0  21966  mndifsplit  21981  chfacfscmulgsum  22205  chfacfpmmulgsum  22209  alexsublem  23391  ovolunlem1  24857  mbfi1fseqlem4  25079  deg1lt  25458  deg1invg  25467  sspz  29575  0lno  29630  pjhth  30233  pjhtheu  30234  pjpreeq  30238  opsqrlem1  30980  pfx1s2  31690  orng0le1  32002  0nellinds  32054  qqh1  32457  dnibndlem5  34934  relowlssretop  35823  mettrifi  36205  rngolz  36370  rngorz  36371  keridl  36480  lfl0f  37520  lkrlss  37546  lkrscss  37549  lkrin  37615  dihpN  39788  djh02  39865  lclkrlem1  39958  lclkr  39985  mon1pid  41508  mon1psubm  41509  minregex  41786  clsneiel1  42360  stoweidlem22  44233  stoweidlem34  44245  sqwvfoura  44439  elaa2lem  44444  nzrneg1ne0  46137  rnglz  46152  zrrnghm  46185  onsetreclem2  47121
  Copyright terms: Public domain W3C validator