ILE Home 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  6552  nq02m  6561  gt0srpr  6831  pitoregt0  6923  axcnre  6953  addgt0  7441  addgegt0  7442  addgtge0  7443  addge0  7444  addgt0i  7478  addge0i  7479  addgegt0i  7480  add20i  7482  mulge0i  7609  recextlem1  7630  recap0  7662  recdivap  7692  recgt1  7861  prodgt0i  7872  prodge0i  7873  iccshftri  8861  iccshftli  8863  iccdili  8865  icccntri  8867  mulexpzap  9269  expaddzap  9273  amgm2  9688
  Copyright terms: Public domain W3C validator