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

Theorem syl2and 500
Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
syl2and.1 (𝜑 → (𝜓𝜒))
syl2and.2 (𝜑 → (𝜃𝜏))
syl2and.3 (𝜑 → ((𝜒𝜏) → 𝜂))
Assertion
Ref Expression
syl2and (𝜑 → ((𝜓𝜃) → 𝜂))

Proof of Theorem syl2and
StepHypRef Expression
1 syl2and.1 . 2 (𝜑 → (𝜓𝜒))
2 syl2and.2 . . 3 (𝜑 → (𝜃𝜏))
3 syl2and.3 . . 3 (𝜑 → ((𝜒𝜏) → 𝜂))
42, 3sylan2d 499 . 2 (𝜑 → ((𝜒𝜃) → 𝜂))
51, 4syland 498 1 (𝜑 → ((𝜓𝜃) → 𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  anim12d  585  ax7  1940  dffi3  8281  cflim2  9029  axpre-sup  9934  xle2add  12032  fzen  12300  rpmulgcd2  15294  pcqmul  15482  initoeu1  16582  termoeu1  16589  plttr  16891  pospo  16894  lublecllem  16909  latjlej12  16988  latmlem12  17004  cygabl  18213  hausnei2  21067  uncmp  21116  itgsubst  23716  dvdsmulf1o  24820  2sqlem8a  25050  axcontlem9  25752  uspgr2wlkeq  26411  numclwlk1lem2f1  27082  shintcli  28037  cvntr  29000  cdj3i  29149  bj-bary1  32795  heicant  33076  itg2addnc  33096  dihmeetlem1N  36059  fmtnofac2lem  40779
  Copyright terms: Public domain W3C validator