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

Theorem mpanr12 423
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 421 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 409 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 is referenced by:  cnvoprab  5883  2dom  6316  phplem4  6349  mulidnq  6545  nq0m0r  6612  nq0a0  6613  addpinq1  6620  0idsr  6910  1idsr  6911  00sr  6912  addresr  6971  mulresr  6972  pitonnlem2  6981  ax0id  7010  recexaplem2  7707  reclt1  7937  crap0  7986  nominpos  8219  expnass  9524  crim  9686  sqrt00  9867  mulcn2  10064  opoe  10207
  Copyright terms: Public domain W3C validator