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 7 . 2 𝜓
43a1i 9 1 (𝜒𝜓)
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  4742  relcoi2  4873  tfrlemi14d  5975  findcard2d  6376  findcard2sd  6377  ac6sfi  6380  cauappcvgprlemladd  6784  caucvgprprlemmu  6821  caucvgsrlemfv  6903  recidpirqlemcalc  6961  recidpirq  6962  q0mod  9270  q1mod  9271  mulp1mod1  9280  m1modnnsub1  9285  modqm1p1mod0  9290  modqltm1p1mod  9291  ibcval5  9595  moddvds  10080  oddnn02np1  10155  oddge22np1  10156  evennn02n  10157  evennn2n  10158
  Copyright terms: Public domain W3C validator