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

Theorem syl2anc2 586
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 585 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  ssnnfiOLD  9120  php4  9163  djulepw  10136  infdjuabs  10150  xrsupss  13237  xrinfmss  13238  trclfv  14894  isumsplit  15733  ram0  16902  0mhm  18638  grpidssd  18831  gexdvds  19374  lsmdisj2  19472  mulgnn0di  19612  odadd1  19634  gsumval3  19692  telgsums  19778  dprdfadd  19807  ringlz  20019  ringrz  20020  lspsneq  20628  dsmmacl  21170  mplsubglem  21428  scmatmhm  21906  mdetuni0  21993  mndifsplit  22008  chfacfscmulgsum  22232  chfacfpmmulgsum  22236  alexsublem  23418  ovolunlem1  24884  mbfi1fseqlem4  25106  deg1lt  25485  deg1invg  25494  sspz  29726  0lno  29781  pjhth  30384  pjhtheu  30385  pjpreeq  30389  opsqrlem1  31131  pfx1s2  31851  orng0le1  32161  0nellinds  32213  qqh1  32630  dnibndlem5  34998  relowlssretop  35884  mettrifi  36266  rngolz  36431  rngorz  36432  keridl  36541  lfl0f  37581  lkrlss  37607  lkrscss  37610  lkrin  37676  dihpN  39849  djh02  39926  lclkrlem1  40019  lclkr  40046  mon1pid  41579  mon1psubm  41580  minregex  41898  clsneiel1  42472  stoweidlem22  44353  stoweidlem34  44365  sqwvfoura  44559  elaa2lem  44564  nzrneg1ne0  46257  rnglz  46272  zrrnghm  46305  onsetreclem2  47241
  Copyright terms: Public domain W3C validator