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  3247  ordtri2orexmid  4268  opthreg  4301  ordtri2or2exmid  4316  fvtp1  5398  nq0m0r  6697  nq02m  6706  gt0srpr  6976  pitoregt0  7068  axcnre  7098  addgt0  7608  addgegt0  7609  addgtge0  7610  addge0  7611  addgt0i  7645  addge0i  7646  addgegt0i  7647  add20i  7649  mulge0i  7776  recextlem1  7797  recap0  7829  recdivap  7862  recgt1  8031  prodgt0i  8042  prodge0i  8043  iccshftri  9082  iccshftli  9084  iccdili  9086  icccntri  9088  mulexpzap  9602  expaddzap  9606  m1expeven  9609  iexpcyc  9665  amgm2  10131  sqnprm  10650
 Copyright terms: Public domain W3C validator