![]() |
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 eqtr 2195 opabss 4064 euotd 4251 wetriext 4573 sosng 4696 xpsspw 4735 brcogw 4792 funimaexglem 5295 funfni 5312 fnco 5320 fnssres 5325 fn0 5331 fnimadisj 5332 fnimaeq0 5333 foco 5444 foimacnv 5475 fvelimab 5568 fvopab3ig 5586 dff3im 5657 dffo4 5660 fmptco 5678 f1eqcocnv 5786 f1ocnv2d 6069 fnexALT 6106 xp1st 6160 xp2nd 6161 tfrlemiubacc 6325 tfri2d 6331 tfr1onlemubacc 6341 tfrcllemubacc 6354 tfri3 6362 ecelqsg 6582 elqsn0m 6597 fidifsnen 6864 recclnq 7379 nq0a0 7444 qreccl 9628 difelfzle 10117 exfzdc 10223 modifeq2int 10369 frec2uzlt2d 10387 1elfz0hash 10767 caucvgrelemcau 10970 recvalap 11087 fzomaxdiflem 11102 2zsupmax 11215 2zinfmin 11232 fsumparts 11459 ntrivcvgap 11537 divconjdvds 11835 ndvdssub 11915 zsupcllemstep 11926 rplpwr 12008 dvdssqlem 12011 eucalgcvga 12038 mulgcddvds 12074 isprm2lem 12096 powm2modprm 12232 coprimeprodsq 12237 pythagtriplem11 12254 pythagtriplem13 12256 grpidd 12691 ismndd 12727 mulgaddcom 12892 isringd 13043 uniopn 13159 ntrval 13270 clsval 13271 neival 13303 restdis 13344 lmbrf 13375 cnpnei 13379 dviaddf 13829 dvimulf 13830 logbgt0b 14044 lgslem4 14064 lgsmod 14087 lgsdir2lem2 14090 lgsdir2 14094 lgsne0 14099 lgsmulsqcoprm 14107 2sqlem4 14114 |
Copyright terms: Public domain | W3C validator |