MPE Home 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 197  df-an 385
This theorem is referenced by:  anim12d  585  ax7  1989  dffi3  8378  cflim2  9123  axpre-sup  10028  xle2add  12127  fzen  12396  rpmulgcd2  15417  pcqmul  15605  initoeu1  16708  termoeu1  16715  plttr  17017  pospo  17020  lublecllem  17035  latjlej12  17114  latmlem12  17130  cygabl  18338  hausnei2  21205  uncmp  21254  itgsubst  23857  dvdsmulf1o  24965  2sqlem8a  25195  axcontlem9  25897  uspgr2wlkeq  26598  shintcli  28316  cvntr  29279  cdj3i  29428  bj-bary1  33292  heicant  33574  itg2addnc  33594  dihmeetlem1N  36896  fmtnofac2lem  41805
  Copyright terms: Public domain W3C validator