![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimpar | Unicode version |
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Ref | Expression |
---|---|
biimpa.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
biimpar |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimpa.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimprd 158 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 124 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: exbiri 382 bitr 472 biadanid 614 eqtr 2207 opabss 4082 euotd 4272 wetriext 4594 sosng 4717 xpsspw 4756 brcogw 4814 funimaexglem 5318 funfni 5335 fnco 5343 fnssres 5348 fn0 5354 fnimadisj 5355 fnimaeq0 5356 foco 5467 foimacnv 5498 fvelimab 5592 fvopab3ig 5610 dff3im 5681 dffo4 5684 fmptco 5702 f1eqcocnv 5812 f1ocnv2d 6097 fnexALT 6135 xp1st 6189 xp2nd 6190 tfrlemiubacc 6354 tfri2d 6360 tfr1onlemubacc 6370 tfrcllemubacc 6383 tfri3 6391 ecelqsg 6613 elqsn0m 6628 fidifsnen 6897 recclnq 7420 nq0a0 7485 qreccl 9671 difelfzle 10163 exfzdc 10269 modifeq2int 10416 frec2uzlt2d 10434 zzlesq 10719 1elfz0hash 10817 caucvgrelemcau 11020 recvalap 11137 fzomaxdiflem 11152 2zsupmax 11265 2zinfmin 11282 fsumparts 11509 ntrivcvgap 11587 divconjdvds 11886 ndvdssub 11966 zsupcllemstep 11977 rplpwr 12059 dvdssqlem 12062 eucalgcvga 12089 mulgcddvds 12125 isprm2lem 12147 powm2modprm 12283 coprimeprodsq 12288 pythagtriplem11 12305 pythagtriplem13 12307 pcadd2 12372 4sqlem11 12432 grpidd 12856 ismndd 12895 mulgaddcom 13083 resghm 13196 conjnsg 13217 isrngd 13304 isringd 13392 01eq0ring 13533 lspsneq0b 13740 lmodindp1 13741 uniopn 13953 ntrval 14062 clsval 14063 neival 14095 restdis 14136 lmbrf 14167 cnpnei 14171 dviaddf 14621 dvimulf 14622 logbgt0b 14836 lgslem4 14857 lgsmod 14880 lgsdir2lem2 14883 lgsdir2 14887 lgsne0 14892 lgsmulsqcoprm 14900 lgseisenlem1 14903 2sqlem4 14918 |
Copyright terms: Public domain | W3C validator |