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  6234  2dom  6804  phplem4  6854  fiintim  6927  mulidnq  7387  nq0m0r  7454  nq0a0  7455  addpinq1  7462  0idsr  7765  1idsr  7766  00sr  7767  addresr  7835  mulresr  7836  pitonnlem2  7845  ax0id  7876  recexaplem2  8607  reclt1  8851  crap0  8913  nominpos  9154  expnass  10622  crim  10862  sqrt00  11044  mulcn2  11315  sin02gt0  11766  opoe  11894  oddprm  12253  pythagtriplem3  12261  pc1  12299  txswaphmeo  13714  sinq34lt0t  14145  cosordlem  14163  lgsne0  14332  lgsdinn0  14342
  Copyright terms: Public domain W3C validator