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 5 . 2  |-  ps
43a1i 9 1  |-  ( ch 
->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6
This theorem is referenced by:  poirr2  4899  relcoi2  5037  tfrlemi14d  6196  tfri1dALT  6214  mapsncnv  6555  findcard2d  6751  findcard2sd  6752  ac6sfi  6758  xpfi  6784  fifo  6834  updjudhcoinlf  6931  updjudhcoinrg  6932  updjud  6933  casefun  6936  omp1eomlem  6945  difinfsnlem  6950  djufun  6955  ctm  6960  ismkvnex  6995  cauappcvgprlemladd  7430  caucvgprprlemmu  7467  caucvgsrlemfv  7563  recidpirqlemcalc  7629  recidpirq  7630  axaddf  7640  axmulf  7641  xaddpnf1  9580  q0mod  10079  q1mod  10080  mulp1mod1  10089  m1modnnsub1  10094  modqm1p1mod0  10099  modqltm1p1mod  10100  bcval5  10460  negfi  10950  xrmaxadd  10981  ege2le3  11287  moddvds  11409  oddnn02np1  11484  oddge22np1  11485  evennn02n  11486  evennn2n  11487  3lcm2e6woprm  11674  6lcm4e12  11675  isprm6  11732  sqrt2irraplemnn  11763  ennnfonelemp1  11825  ennnfonelemkh  11831  ennnfonelemex  11833  exmidunben  11845  strslfv  11909  strleund  11953  cnbl0  12609  negfcncf  12664  cnrehmeocntop  12668  dvidlemap  12735  dvid  12737  dvmulxxbr  12741  dvexp  12750  sincn  12764  coscn  12765  pwf1oexmid  13028  nninfsellemdc  13040  trilpolemlt1  13068
  Copyright terms: Public domain W3C validator