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

Theorem syl2and 610
 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 607 . 2 (𝜑 → ((𝜒𝜃) → 𝜂))
51, 4syland 605 1 (𝜑 → ((𝜓𝜃) → 𝜂))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  anim12d  611  ax7  2023  dffi3  8883  cflim2  9674  axpre-sup  10580  xle2add  12640  fzen  12919  rpmulgcd2  15989  pcqmul  16179  initoeu1  17262  termoeu1  17269  plttr  17571  pospo  17574  lublecllem  17589  latjlej12  17668  latmlem12  17684  cygablOLD  19002  hausnei2  21956  uncmp  22006  itgsubst  24650  dvdsmulf1o  25777  2sqlem8a  26007  axcontlem9  26764  uspgr2wlkeq  27433  shintcli  29110  cvntr  30073  cdj3i  30222  f1resrcmplf1dlem  32433  satffunlem  32722  bj-bary1  34687  heicant  35050  itg2addnc  35069  dihmeetlem1N  38544  fmtnofac2lem  44024  2itscp  45134
 Copyright terms: Public domain W3C validator