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: 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: exbiri 379 bitr 463 eqtr 2155 opabss 3987 euotd 4171 wetriext 4486 sosng 4607 xpsspw 4646 brcogw 4703 funimaexglem 5201 funfni 5218 fnco 5226 fnssres 5231 fn0 5237 fnimadisj 5238 fnimaeq0 5239 foco 5350 foimacnv 5378 fvelimab 5470 fvopab3ig 5488 dff3im 5558 dffo4 5561 fmptco 5579 f1eqcocnv 5685 f1ocnv2d 5967 fnexALT 6004 xp1st 6056 xp2nd 6057 tfrlemiubacc 6220 tfri2d 6226 tfr1onlemubacc 6236 tfrcllemubacc 6249 tfri3 6257 ecelqsg 6475 elqsn0m 6490 fidifsnen 6757 recclnq 7193 nq0a0 7258 qreccl 9427 difelfzle 9904 exfzdc 10010 modifeq2int 10152 frec2uzlt2d 10170 1elfz0hash 10545 caucvgrelemcau 10745 recvalap 10862 fzomaxdiflem 10877 2zsupmax 10990 fsumparts 11232 ntrivcvgap 11310 divconjdvds 11536 ndvdssub 11616 zsupcllemstep 11627 rplpwr 11704 dvdssqlem 11707 eucalgcvga 11728 mulgcddvds 11764 isprm2lem 11786 uniopn 12157 ntrval 12268 clsval 12269 neival 12301 restdis 12342 lmbrf 12373 cnpnei 12377 dviaddf 12827 dvimulf 12828 |
Copyright terms: Public domain | W3C validator |