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

Theorem mpanr12 436
 Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1 𝜓
mpanr12.2 𝜒
mpanr12.3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr12 (𝜑𝜃)

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2 𝜒
2 mpanr12.1 . . 3 𝜓
3 mpanr12.3 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3mpanr1 434 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 422 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:  cnvoprab  6171  2dom  6739  phplem4  6789  fiintim  6862  mulidnq  7288  nq0m0r  7355  nq0a0  7356  addpinq1  7363  0idsr  7666  1idsr  7667  00sr  7668  addresr  7736  mulresr  7737  pitonnlem2  7746  ax0id  7777  recexaplem2  8505  reclt1  8746  crap0  8808  nominpos  9049  expnass  10502  crim  10735  sqrt00  10917  mulcn2  11186  sin02gt0  11637  opoe  11759  txswaphmeo  12660  sinq34lt0t  13091  cosordlem  13109
 Copyright terms: Public domain W3C validator