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

Theorem mp1i 10
Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)
Hypotheses
Ref Expression
mp1i.a  |-  ph
mp1i.b  |-  ( ph  ->  ps )
Assertion
Ref Expression
mp1i  |-  ( ch 
->  ps )

Proof of Theorem mp1i
StepHypRef Expression
1 mp1i.a . . 3  |-  ph
2 mp1i.b . . 3  |-  ( ph  ->  ps )
31, 2ax-mp 7 . 2  |-  ps
43a1i 9 1  |-  ( ch 
->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-mp 7
This theorem is referenced by:  poirr2  4745  relcoi2  4876  tfrlemi14d  5978  findcard2d  6379  findcard2sd  6380  ac6sfi  6383  cauappcvgprlemladd  6814  caucvgprprlemmu  6851  caucvgsrlemfv  6933  recidpirqlemcalc  6991  recidpirq  6992  q0mod  9305  q1mod  9306  mulp1mod1  9315  m1modnnsub1  9320  modqm1p1mod0  9325  modqltm1p1mod  9326  ibcval5  9631  moddvds  10117  oddnn02np1  10192  oddge22np1  10193  evennn02n  10194  evennn2n  10195
  Copyright terms: Public domain W3C validator