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

Theorem mpanr12 439
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 437 . 2 ((𝜑𝜒) → 𝜃)
51, 4mpan2 425 1 (𝜑𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  cnvoprab  6237  2dom  6807  phplem4  6857  fiintim  6930  mulidnq  7390  nq0m0r  7457  nq0a0  7458  addpinq1  7465  0idsr  7768  1idsr  7769  00sr  7770  addresr  7838  mulresr  7839  pitonnlem2  7848  ax0id  7879  recexaplem2  8611  reclt1  8855  crap0  8917  nominpos  9158  expnass  10628  crim  10869  sqrt00  11051  mulcn2  11322  sin02gt0  11773  opoe  11902  oddprm  12261  pythagtriplem3  12269  pc1  12307  txswaphmeo  13860  sinq34lt0t  14291  cosordlem  14309  lgsne0  14478  lgsdinn0  14488
  Copyright terms: Public domain W3C validator