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

Theorem mpanl1 425
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 307 . 2 (𝜓 → (𝜑𝜓))
3 mpanl1.2 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
42, 3sylan 277 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  mpanl12  427  ercnv  6267  rec11api  8162  divdiv23apzi  8174  recp1lt1  8298  divgt0i  8309  divge0i  8310  ltreci  8311  lereci  8312  lt2msqi  8313  le2msqi  8314  msq11i  8315  ltdiv23i  8325  fnn0ind  8798  elfzp1b  9444  elfzm1b  9445  sqrt11i  10464  sqrtmuli  10465  sqrtmsq2i  10467  sqrtlei  10468  sqrtlti  10469
  Copyright terms: Public domain W3C validator