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

Theorem mpanl12 414
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 412 . 2 ((ψ χ) → θ)
51, 4mpan 402 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  3192  ordtri2orexmid  4191  opthreg  4214  fvtp1  5293  nq0m0r  6305  nq02m  6313  gt0srpr  6489  axcnre  6569  addgt0  7028  addgegt0  7029  addgtge0  7030  addge0  7031  addgt0i  7063  addge0i  7064  addgegt0i  7065
  Copyright terms: Public domain W3C validator