![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > imbi2d | Unicode version |
Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
imbid.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imbi2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1d 22 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm5.74d 238 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: imbi12d 311 imbi2 314 pm5.42 531 orbi2d 682 con3th 924 19.23tOLD 1819 ax12olem6 1932 ax11v2 1992 ax15 2021 nfsb4t 2080 sbcom 2089 ax11vALT 2097 sbcom2 2114 ax11eq 2193 ax11el 2194 ax11indalem 2197 ax11inda2ALT 2198 ax11inda 2200 ax11v2-o 2201 mo 2226 2mo 2282 2eu6 2289 2gencl 2888 3gencl 2889 vtocl2gf 2916 vtocl3gf 2917 eqeu 3007 mo2icl 3015 euind 3023 reu7 3031 reuind 3039 sbctt 3108 sbcnestgf 3183 r19.36zv 3650 dedth2h 3704 dedth3h 3705 dedth4h 3706 elint 3932 elintrabg 3939 intab 3956 preq12bg 4128 nncaddccl 4419 nndisjeq 4429 ltfintri 4466 ssfin 4470 evenodddisjlem1 4515 evenodddisj 4516 nnadjoin 4520 tfinnn 4534 spfinsfincl 4539 spfininduct 4540 vtoclr 4816 raliunxp 4823 2optocl 4839 3optocl 4840 fneu 5187 fvelimab 5370 fnressn 5438 fressnfv 5439 f1fveq 5473 funsi 5520 ndmovcl 5614 caovcan 5628 caovord 5629 fvmptss 5705 trtxp 5781 oqelins4 5794 fntxp 5804 qrpprod 5836 fnpprod 5843 fnfullfunlem1 5856 frd 5922 2ecoptocl 5997 3ecoptocl 5998 sbthlem2 6204 leconnnc 6218 addcdi 6250 nchoicelem17 6305 nchoicelem19 6307 |
Copyright terms: Public domain | W3C validator |