Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpani GIF version

Theorem mpani 414
 Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpani.1 𝜓
mpani.2 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
mpani (𝜑 → (𝜒𝜃))

Proof of Theorem mpani
StepHypRef Expression
1 mpani.1 . . 3 𝜓
21a1i 9 . 2 (𝜑𝜓)
3 mpani.2 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
42, 3mpand 413 1 (𝜑 → (𝜒𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  mp2ani  416  mulgt1  7904  recgt1i  7939  recreclt  7941  nngt0  8015  nnrecgt0  8027  elnnnn0c  8284  elnnz1  8325  recnz  8391  uz3m2nn  8611  ledivge1le  8750  expubnd  9477  expnbnd  9540  expnlbnd  9541  oddge22np1  10193
 Copyright terms: Public domain W3C validator