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

Theorem mpanr1 435
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 433 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  437  axcnre  7843  rec11api  8670  divdiv23apzi  8682  recp1lt1  8815  divgt0i  8826  divge0i  8827  ltreci  8828  lereci  8829  lt2msqi  8830  le2msqi  8831  msq11i  8832  ltdiv23i  8842  ge0gtmnf  9780  sqrt11i  11096  sqrtmuli  11097  sqrtmsq2i  11099  sqrtlei  11100  sqrtlti  11101  cos01gt0  11725
  Copyright terms: Public domain W3C validator