![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp1i | Unicode 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: ![]() |
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 |