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

Theorem mp2ani 698
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 696 . 2 (𝜑 → (𝜒𝜃))
51, 4mpi 20 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  inf0  9659  dfom3  9685  dfac5lem4  10164  dfac5lem4OLD  10166  dfac9  10175  cflem  10283  cflemOLD  10284  canthp1lem2  10691  addsrpr  11113  mulsrpr  11114  trclublem  15031  gcdaddmlem  16558  tgjustf  28496  sto1i  32265  stji1i  32271  kur14lem9  35199  dfon2lem4  35768  rtrclex  43607  comptiunov2i  43696
  Copyright terms: Public domain W3C validator