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

Theorem syl2and 499
 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 498 . 2 (𝜑 → ((𝜒𝜃) → 𝜂))
51, 4syland 497 1 (𝜑 → ((𝜓𝜃) → 𝜂))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  anim12d  584  ax7  1930  dffi3  8220  cflim2  8968  axpre-sup  9869  xle2add  11961  fzen  12229  rpmulgcd2  15208  pcqmul  15396  initoeu1  16484  termoeu1  16491  plttr  16793  pospo  16796  lublecllem  16811  latjlej12  16890  latmlem12  16906  cygabl  18115  hausnei2  20967  uncmp  21016  itgsubst  23616  dvdsmulf1o  24720  2sqlem8a  24950  axcontlem9  25652  usg2wotspth  26411  numclwlk1lem2f1  26621  shintcli  27572  cvntr  28535  cdj3i  28684  bj-bary1  32339  heicant  32614  itg2addnc  32634  dihmeetlem1N  35597  fmtnofac2lem  40018  uspgr2wlkeq  40854  av-numclwlk1lem2f1  41524
 Copyright terms: Public domain W3C validator