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

Theorem mpanr1 437
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 400 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 435 1 ((𝜑𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  mpanr12  439  axcnre  7879  rec11api  8708  divdiv23apzi  8720  recp1lt1  8854  divgt0i  8865  divge0i  8866  ltreci  8867  lereci  8868  lt2msqi  8869  le2msqi  8870  msq11i  8871  ltdiv23i  8881  ge0gtmnf  9821  sqrt11i  11136  sqrtmuli  11137  sqrtmsq2i  11139  sqrtlei  11140  sqrtlti  11141  cos01gt0  11765
  Copyright terms: Public domain W3C validator