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

Theorem syl2and 589
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 586 . 2 (𝜑 → ((𝜒𝜃) → 𝜂))
51, 4syland 584 1 (𝜑 → ((𝜓𝜃) → 𝜂))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  anim12d  590  ax7  2101  dffi3  8494  cflim2  9288  axpre-sup  10193  xle2add  12295  fzen  12566  rpmulgcd2  15578  pcqmul  15766  initoeu1  16869  termoeu1  16876  plttr  17179  pospo  17182  lublecllem  17197  latjlej12  17276  latmlem12  17292  cygabl  18500  hausnei2  21379  uncmp  21428  itgsubst  24033  dvdsmulf1o  25142  2sqlem8a  25372  axcontlem9  26074  uspgr2wlkeq  26778  shintcli  28529  cvntr  29492  cdj3i  29641  bj-bary1  33500  heicant  33778  itg2addnc  33797  dihmeetlem1N  37101  fmtnofac2lem  42009
  Copyright terms: Public domain W3C validator