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

Theorem mpanr1 433
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 397 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
41, 3mpanl2 431 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  435  axcnre  7696  rec11api  8520  divdiv23apzi  8532  recp1lt1  8664  divgt0i  8675  divge0i  8676  ltreci  8677  lereci  8678  lt2msqi  8679  le2msqi  8680  msq11i  8681  ltdiv23i  8691  ge0gtmnf  9613  sqrt11i  10911  sqrtmuli  10912  sqrtmsq2i  10914  sqrtlei  10915  sqrtlti  10916  cos01gt0  11476
  Copyright terms: Public domain W3C validator