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 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:  inf0  9158  dfom3  9184  dfac5lem4  9627  dfac9  9637  cflem  9747  canthp1lem2  10154  addsrpr  10576  mulsrpr  10577  trclublem  14445  gcdaddmlem  15968  tgjustf  26419  sto1i  30171  stji1i  30177  kur14lem9  32747  dfon2lem4  33334  rtrclex  40762  comptiunov2i  40852
  Copyright terms: Public domain W3C validator