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

Theorem mpanl1 430
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 312 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 281 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:  mpanl12  432  ercnv  6418  rec11api  8481  divdiv23apzi  8493  recp1lt1  8625  divgt0i  8636  divge0i  8637  ltreci  8638  lereci  8639  lt2msqi  8640  le2msqi  8641  msq11i  8642  ltdiv23i  8652  fnn0ind  9135  elfzp1b  9845  elfzm1b  9846  sqrt11i  10872  sqrtmuli  10873  sqrtmsq2i  10875  sqrtlei  10876  sqrtlti  10877
  Copyright terms: Public domain W3C validator