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

Theorem syl2and 601
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 598 . 2 (𝜑 → ((𝜒𝜃) → 𝜂))
51, 4syland 596 1 (𝜑 → ((𝜓𝜃) → 𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386
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 199  df-an 387
This theorem is referenced by:  anim12d  602  ax7  2063  dffi3  8625  cflim2  9420  axpre-sup  10326  xle2add  12401  fzen  12675  rpmulgcd2  15775  pcqmul  15962  initoeu1  17046  termoeu1  17053  plttr  17356  pospo  17359  lublecllem  17374  latjlej12  17453  latmlem12  17469  cygabl  18678  hausnei2  21565  uncmp  21615  itgsubst  24249  dvdsmulf1o  25372  2sqlem8a  25602  axcontlem9  26321  uspgr2wlkeq  26993  shintcli  28760  cvntr  29723  cdj3i  29872  bj-bary1  33760  heicant  34070  itg2addnc  34089  dihmeetlem1N  37444  fmtnofac2lem  42501  2itscp  43517
  Copyright terms: Public domain W3C validator