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

Theorem mpanr1 434
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
mpanr1.1 𝜓
mpanr1.2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr1 ((𝜑𝜒) → 𝜃)

Proof of Theorem mpanr1
StepHypRef Expression
1 mpanr1.1 . 2 𝜓
2 mpanr1.2 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
32anassrs 398 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 432 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  mpanr12  436  axcnre  7802  rec11api  8627  divdiv23apzi  8639  recp1lt1  8771  divgt0i  8782  divge0i  8783  ltreci  8784  lereci  8785  lt2msqi  8786  le2msqi  8787  msq11i  8788  ltdiv23i  8798  ge0gtmnf  9728  sqrt11i  11036  sqrtmuli  11037  sqrtmsq2i  11039  sqrtlei  11040  sqrtlti  11041  cos01gt0  11663
  Copyright terms: Public domain W3C validator