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

Theorem mpanr1 421
 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 386 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 419 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:  mpanr12  423  axcnre  7013  rec11api  7804  divdiv23apzi  7816  recp1lt1  7940  divgt0i  7951  divge0i  7952  ltreci  7953  lereci  7954  lt2msqi  7955  le2msqi  7956  msq11i  7957  ltdiv23i  7967  ge0gtmnf  8837  sqrt11i  9959  sqrtmuli  9960  sqrtmsq2i  9962  sqrtlei  9963  sqrtlti  9964
 Copyright terms: Public domain W3C validator