Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpanl12 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  3219  ordtri2orexmid  4248  opthreg  4280  ordtri2or2exmid  4296  fvtp1  5372  nq0m0r  6554  nq02m  6563  gt0srpr  6833  pitoregt0  6925  axcnre  6955  addgt0  7443  addgegt0  7444  addgtge0  7445  addge0  7446  addgt0i  7480  addge0i  7481  addgegt0i  7482  add20i  7484  mulge0i  7611  recextlem1  7632  recap0  7664  recdivap  7694  recgt1  7863  prodgt0i  7874  prodge0i  7875  iccshftri  8863  iccshftli  8865  iccdili  8867  icccntri  8869  mulexpzap  9295  expaddzap  9299  amgm2  9714
 Copyright terms: Public domain W3C validator