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

Theorem mpanr12 435
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 433 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 421 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  6099  2dom  6667  phplem4  6717  fiintim  6785  mulidnq  7165  nq0m0r  7232  nq0a0  7233  addpinq1  7240  0idsr  7543  1idsr  7544  00sr  7545  addresr  7613  mulresr  7614  pitonnlem2  7623  ax0id  7654  recexaplem2  8381  reclt1  8622  crap0  8684  nominpos  8925  expnass  10366  crim  10598  sqrt00  10780  mulcn2  11049  sin02gt0  11397  opoe  11519  txswaphmeo  12417  sinq34lt0t  12839  cosordlem  12857
  Copyright terms: Public domain W3C validator