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

Theorem mpanl12 432
 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 430 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 420 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:  reuun1  3358  ordtri2orexmid  4438  opthreg  4471  ordtri2or2exmid  4486  fvtp1  5631  nq0m0r  7271  nq02m  7280  gt0srpr  7563  map2psrprg  7620  pitoregt0  7664  axcnre  7696  addgt0  8217  addgegt0  8218  addgtge0  8219  addge0  8220  addgt0i  8257  addge0i  8258  addgegt0i  8259  add20i  8261  mulge0i  8389  recextlem1  8419  recap0  8452  recdivap  8485  recgt1  8662  prodgt0i  8673  prodge0i  8674  iccshftri  9785  iccshftli  9787  iccdili  9789  icccntri  9791  mulexpzap  10340  expaddzap  10344  m1expeven  10347  iexpcyc  10404  amgm2  10897  ege2le3  11384  sqnprm  11823  lmres  12427
 Copyright terms: Public domain W3C validator