Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimparc | Unicode version |
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
Ref | Expression |
---|---|
biimpa.1 |
Ref | Expression |
---|---|
biimparc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimpa.1 | . . 3 | |
2 | 1 | biimprcd 159 | . 2 |
3 | 2 | imp 123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biantr 937 elrab3t 2867 difprsnss 3694 elpw2g 4117 elon2 4336 ideqg 4737 elrnmpt1s 4836 elrnmptg 4838 fun11iun 5435 eqfnfv2 5566 fmpt 5617 elunirn 5716 spc2ed 6180 tposfo2 6214 tposf12 6216 dom2lem 6717 enfii 6819 ac6sfi 6843 ltexprlemm 7520 elreal2 7750 fihasheqf1oi 10662 fprod2dlemstep 11519 bastop2 12495 |
Copyright terms: Public domain | W3C validator |