Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bi2anan9 | Unicode version |
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
bi2an9.1 | |
bi2an9.2 |
Ref | Expression |
---|---|
bi2anan9 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi2an9.1 | . . 3 | |
2 | 1 | anbi1d 460 | . 2 |
3 | bi2an9.2 | . . 3 | |
4 | 3 | anbi2d 459 | . 2 |
5 | 2, 4 | sylan9bb 457 | 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: bi2anan9r 596 rspc2gv 2796 ralprg 3569 raltpg 3571 prssg 3672 prsspwg 3674 opelopab2a 4182 opelxp 4564 eqrel 4623 eqrelrel 4635 brcog 4701 dff13 5662 resoprab2 5861 ovig 5885 dfoprab4f 6084 f1o2ndf1 6118 eroveu 6513 th3qlem1 6524 th3qlem2 6525 th3q 6527 oviec 6528 endisj 6711 dfplpq2 7155 dfmpq2 7156 ordpipqqs 7175 enq0enq 7232 mulnnnq0 7251 ltsrprg 7548 axcnre 7682 axmulgt0 7829 addltmul 8949 ltxr 9555 sumsqeq0 10364 mul0inf 11005 dvds2lem 11494 opoe 11581 omoe 11582 opeo 11583 omeo 11584 gcddvds 11641 dfgcd2 11691 txbasval 12425 cnmpt12 12445 cnmpt22 12452 |
Copyright terms: Public domain | W3C validator |