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

Theorem mpanl1 418
Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpanl1.1 𝜑
mpanl1.2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
mpanl1 ((𝜓𝜒) → 𝜃)

Proof of Theorem mpanl1
StepHypRef Expression
1 mpanl1.1 . . 3 𝜑
21jctl 301 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 271 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:  mpanl12  420  ercnv  6158  rec11api  7804  divdiv23apzi  7816  recp1lt1  7940  divgt0i  7951  divge0i  7952  ltreci  7953  lereci  7954  lt2msqi  7955  le2msqi  7956  msq11i  7957  ltdiv23i  7967  fnn0ind  8413  elfzp1b  9061  elfzm1b  9062  sqrt11i  9959  sqrtmuli  9960  sqrtmsq2i  9962  sqrtlei  9963  sqrtlti  9964
  Copyright terms: Public domain W3C validator