![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp1i | GIF version |
Description: Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.) |
Ref | Expression |
---|---|
mp1i.a | ⊢ 𝜑 |
mp1i.b | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
mp1i | ⊢ (𝜒 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp1i.a | . . 3 ⊢ 𝜑 | |
2 | mp1i.b | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | ax-mp 7 | . 2 ⊢ 𝜓 |
4 | 3 | a1i 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 4767 relcoi2 4898 tfrlemi14d 6002 tfri1dALT 6020 findcard2d 6447 findcard2sd 6448 ac6sfi 6454 xpfi 6472 cauappcvgprlemladd 6962 caucvgprprlemmu 6999 caucvgsrlemfv 7081 recidpirqlemcalc 7139 recidpirq 7140 q0mod 9489 q1mod 9490 mulp1mod1 9499 m1modnnsub1 9504 modqm1p1mod0 9509 modqltm1p1mod 9510 ibcval5 9839 negfi 10311 moddvds 10412 oddnn02np1 10487 oddge22np1 10488 evennn02n 10489 evennn2n 10490 3lcm2e6woprm 10675 6lcm4e12 10676 isprm6 10733 sqrt2irraplemnn 10764 |
Copyright terms: Public domain | W3C validator |