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

Theorem mp1i 10
Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.)
Hypotheses
Ref Expression
mp1i.a 𝜑
mp1i.b (𝜑𝜓)
Assertion
Ref Expression
mp1i (𝜒𝜓)

Proof of Theorem mp1i
StepHypRef Expression
1 mp1i.a . . 3 𝜑
2 mp1i.b . . 3 (𝜑𝜓)
31, 2ax-mp 5 . 2 𝜓
43a1i 9 1 (𝜒𝜓)
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  4901  relcoi2  5039  tfrlemi14d  6198  tfri1dALT  6216  mapsncnv  6557  findcard2d  6753  findcard2sd  6754  ac6sfi  6760  xpfi  6786  fifo  6836  updjudhcoinlf  6933  updjudhcoinrg  6934  updjud  6935  casefun  6938  omp1eomlem  6947  difinfsnlem  6952  djufun  6957  ctm  6962  ismkvnex  6997  cauappcvgprlemladd  7434  caucvgprprlemmu  7471  caucvgsrlemfv  7567  recidpirqlemcalc  7633  recidpirq  7634  axaddf  7644  axmulf  7645  xaddpnf1  9597  q0mod  10096  q1mod  10097  mulp1mod1  10106  m1modnnsub1  10111  modqm1p1mod0  10116  modqltm1p1mod  10117  bcval5  10477  negfi  10967  xrmaxadd  10998  ege2le3  11304  moddvds  11429  oddnn02np1  11504  oddge22np1  11505  evennn02n  11506  evennn2n  11507  3lcm2e6woprm  11694  6lcm4e12  11695  isprm6  11752  sqrt2irraplemnn  11784  ennnfonelemp1  11846  ennnfonelemkh  11852  ennnfonelemex  11854  exmidunben  11866  strslfv  11930  strleund  11974  cnbl0  12630  negfcncf  12685  cnrehmeocntop  12689  dvidlemap  12756  dvid  12758  dvmulxxbr  12762  dvexp  12771  sincn  12785  coscn  12786  coseq0q4123  12842  tangtx  12846  cosordlem  12857  pwf1oexmid  13121  nninfsellemdc  13133  trilpolemlt1  13161
  Copyright terms: Public domain W3C validator