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

Theorem mpanr12 430
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1  |-  ps
mpanr12.2  |-  ch
mpanr12.3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
mpanr12  |-  ( ph  ->  th )

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2  |-  ch
2 mpanr12.1 . . 3  |-  ps
3 mpanr12.3 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3mpanr1 428 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 416 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  cnvoprab  5934  2dom  6452  phplem4  6501  mulidnq  6851  nq0m0r  6918  nq0a0  6919  addpinq1  6926  0idsr  7216  1idsr  7217  00sr  7218  addresr  7277  mulresr  7278  pitonnlem2  7287  ax0id  7316  recexaplem2  8019  reclt1  8251  crap0  8312  nominpos  8545  expnass  9896  crim  10119  sqrt00  10300  mulcn2  10525  opoe  10675
  Copyright terms: Public domain W3C validator