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  4824  relcoi2  4961  tfrlemi14d  6098  tfri1dALT  6116  mapsncnv  6452  findcard2d  6607  findcard2sd  6608  ac6sfi  6614  xpfi  6640  updjudhcoinlf  6771  updjudhcoinrg  6772  updjud  6773  casefun  6776  djufun  6784  cauappcvgprlemladd  7217  caucvgprprlemmu  7254  caucvgsrlemfv  7336  recidpirqlemcalc  7394  recidpirq  7395  q0mod  9762  q1mod  9763  mulp1mod1  9772  m1modnnsub1  9777  modqm1p1mod0  9782  modqltm1p1mod  9783  ibcval5  10171  negfi  10659  ege2le3  10961  moddvds  11083  oddnn02np1  11158  oddge22np1  11159  evennn02n  11160  evennn2n  11161  3lcm2e6woprm  11346  6lcm4e12  11347  isprm6  11404  sqrt2irraplemnn  11435  strslfv  11538  strleund  11581  nninfsellemdc  11902
  Copyright terms: Public domain W3C validator