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

Theorem mpanl12 412
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mpanl12.1 φ
mpanl12.2 ψ
mpanl12.3 (((φ ψ) χ) → θ)
Assertion
Ref Expression
mpanl12 (χθ)

Proof of Theorem mpanl12
StepHypRef Expression
1 mpanl12.2 . 2 ψ
2 mpanl12.1 . . 3 φ
3 mpanl12.3 . . 3 (((φ ψ) χ) → θ)
42, 3mpanl1 410 . 2 ((ψ χ) → θ)
51, 4mpan 400 1 (χθ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  reuun1  3213  ordtri2orexmid  4211  opthreg  4234  fvtp1  5315  nq0m0r  6438  nq02m  6447  gt0srpr  6656  axcnre  6745  addgt0  7218  addgegt0  7219  addgtge0  7220  addge0  7221  addgt0i  7255  addge0i  7256  addgegt0i  7257  add20i  7259  mulge0i  7384  recextlem1  7394  recap0  7426  recdivap  7456  recgt1  7624  prodgt0i  7635  prodge0i  7636  iccshftri  8613  iccshftli  8615  iccdili  8617  icccntri  8619  mulexpzap  8929  expaddzap  8933
  Copyright terms: Public domain W3C validator