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

Theorem mpanl12 427
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 425 . 2 ((𝜓𝜒) → 𝜃)
51, 4mpan 415 1 (𝜒𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  reuun1  3270  ordtri2orexmid  4311  opthreg  4344  ordtri2or2exmid  4359  fvtp1  5463  nq0m0r  6952  nq02m  6961  gt0srpr  7231  pitoregt0  7323  axcnre  7353  addgt0  7863  addgegt0  7864  addgtge0  7865  addge0  7866  addgt0i  7900  addge0i  7901  addgegt0i  7902  add20i  7904  mulge0i  8031  recextlem1  8052  recap0  8084  recdivap  8117  recgt1  8286  prodgt0i  8297  prodge0i  8298  iccshftri  9337  iccshftli  9339  iccdili  9341  icccntri  9343  mulexpzap  9886  expaddzap  9890  m1expeven  9893  iexpcyc  9949  amgm2  10439  sqnprm  10984
  Copyright terms: Public domain W3C validator