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

Theorem mpanr12 433
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 431 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 419 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  6097  2dom  6665  phplem4  6715  fiintim  6783  mulidnq  7161  nq0m0r  7228  nq0a0  7229  addpinq1  7236  0idsr  7539  1idsr  7540  00sr  7541  addresr  7609  mulresr  7610  pitonnlem2  7619  ax0id  7650  recexaplem2  8373  reclt1  8611  crap0  8673  nominpos  8908  expnass  10338  crim  10570  sqrt00  10752  mulcn2  11021  sin02gt0  11369  opoe  11488  txswaphmeo  12385
  Copyright terms: Public domain W3C validator