![]() |
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 157 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | imp 123 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: exbiri 377 bitr 461 eqtr 2132 opabss 3952 euotd 4136 wetriext 4451 sosng 4572 xpsspw 4611 brcogw 4668 funimaexglem 5164 funfni 5181 fnco 5189 fnssres 5194 fn0 5200 fnimadisj 5201 fnimaeq0 5202 foco 5313 foimacnv 5341 fvelimab 5431 fvopab3ig 5449 dff3im 5519 dffo4 5522 fmptco 5540 f1eqcocnv 5646 f1ocnv2d 5928 fnexALT 5965 xp1st 6017 xp2nd 6018 tfrlemiubacc 6181 tfri2d 6187 tfr1onlemubacc 6197 tfrcllemubacc 6210 tfri3 6218 ecelqsg 6436 elqsn0m 6451 fidifsnen 6717 recclnq 7148 nq0a0 7213 qreccl 9336 difelfzle 9804 exfzdc 9910 modifeq2int 10052 frec2uzlt2d 10070 1elfz0hash 10445 caucvgrelemcau 10644 recvalap 10761 fzomaxdiflem 10776 2zsupmax 10889 fsumparts 11131 divconjdvds 11395 ndvdssub 11475 zsupcllemstep 11486 rplpwr 11561 dvdssqlem 11564 eucalgcvga 11585 mulgcddvds 11621 isprm2lem 11643 uniopn 12011 ntrval 12122 clsval 12123 neival 12155 restdis 12196 lmbrf 12226 cnpnei 12230 dviaddf 12624 dvimulf 12625 |
Copyright terms: Public domain | W3C validator |