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  6450  rec11api  8525  divdiv23apzi  8537  recp1lt1  8669  divgt0i  8680  divge0i  8681  ltreci  8682  lereci  8683  lt2msqi  8684  le2msqi  8685  msq11i  8686  ltdiv23i  8696  fnn0ind  9179  elfzp1b  9889  elfzm1b  9890  sqrt11i  10916  sqrtmuli  10917  sqrtmsq2i  10919  sqrtlei  10920  sqrtlti  10921
 Copyright terms: Public domain W3C validator