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

Theorem mpanr12 415
 Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1 𝜓
mpanr12.2 𝜒
mpanr12.3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr12 (𝜑𝜃)

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2 𝜒
2 mpanr12.1 . . 3 𝜓
3 mpanr12.3 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3mpanr1 413 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 401 1 (𝜑𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem is referenced by:  2dom  6285  phplem4  6318  mulidnq  6487  nq0m0r  6554  nq0a0  6555  addpinq1  6562  0idsr  6852  1idsr  6853  00sr  6854  addresr  6913  mulresr  6914  pitonnlem2  6923  ax0id  6952  recexaplem2  7633  reclt1  7862  crap0  7910  nominpos  8162  expnass  9357  crim  9458  sqrt00  9638  mulcn2  9833
 Copyright terms: Public domain W3C validator