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  4837  relcoi2  4974  tfrlemi14d  6112  tfri1dALT  6130  mapsncnv  6466  findcard2d  6661  findcard2sd  6662  ac6sfi  6668  xpfi  6694  updjudhcoinlf  6825  updjudhcoinrg  6826  updjud  6827  casefun  6830  djufun  6840  ctm  6845  cauappcvgprlemladd  7278  caucvgprprlemmu  7315  caucvgsrlemfv  7397  recidpirqlemcalc  7455  recidpirq  7456  q0mod  9823  q1mod  9824  mulp1mod1  9833  m1modnnsub1  9838  modqm1p1mod0  9843  modqltm1p1mod  9844  ibcval5  10232  negfi  10720  ege2le3  11022  moddvds  11144  oddnn02np1  11219  oddge22np1  11220  evennn02n  11221  evennn2n  11222  3lcm2e6woprm  11407  6lcm4e12  11408  isprm6  11465  sqrt2irraplemnn  11496  strslfv  11599  strleund  11643  nninfsellemdc  12174
  Copyright terms: Public domain W3C validator