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

Theorem mp2ani 694
 Description: An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2ani.1 𝜓
mp2ani.2 𝜒
mp2ani.3 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
mp2ani (𝜑𝜃)

Proof of Theorem mp2ani
StepHypRef Expression
1 mp2ani.2 . 2 𝜒
2 mp2ani.1 . . 3 𝜓
3 mp2ani.3 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
42, 3mpani 692 . 2 (𝜑 → (𝜒𝜃))
51, 4mpi 20 1 (𝜑𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396 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 208  df-an 397 This theorem is referenced by:  dfom3  9099  dfac5lem4  9541  dfac9  9551  cflem  9657  canthp1lem2  10064  addsrpr  10486  mulsrpr  10487  trclublem  14345  gcdaddmlem  15862  tgjustf  26173  sto1i  29927  stji1i  29933  kur14lem9  32345  dfon2lem4  32915  rtrclex  39842  comptiunov2i  39916
 Copyright terms: Public domain W3C validator