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

Theorem mpanr12 435
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 433 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 421 1  |-  ( ph  ->  th )
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  6131  2dom  6699  phplem4  6749  fiintim  6817  mulidnq  7209  nq0m0r  7276  nq0a0  7277  addpinq1  7284  0idsr  7587  1idsr  7588  00sr  7589  addresr  7657  mulresr  7658  pitonnlem2  7667  ax0id  7698  recexaplem2  8425  reclt1  8666  crap0  8728  nominpos  8969  expnass  10410  crim  10642  sqrt00  10824  mulcn2  11093  sin02gt0  11481  opoe  11603  txswaphmeo  12504  sinq34lt0t  12934  cosordlem  12952
  Copyright terms: Public domain W3C validator