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 581 rspc2gv 2775 ralprg 3544 raltpg 3546 prssg 3647 prsspwg 3649 opelopab2a 4157 opelxp 4539 eqrel 4598 eqrelrel 4610 brcog 4676 dff13 5637 resoprab2 5836 ovig 5860 dfoprab4f 6059 f1o2ndf1 6093 eroveu 6488 th3qlem1 6499 th3qlem2 6500 th3q 6502 oviec 6503 endisj 6686 dfplpq2 7130 dfmpq2 7131 ordpipqqs 7150 enq0enq 7207 mulnnnq0 7226 ltsrprg 7523 axcnre 7657 axmulgt0 7804 addltmul 8914 ltxr 9517 sumsqeq0 10326 mul0inf 10967 dvds2lem 11417 opoe 11504 omoe 11505 opeo 11506 omeo 11507 gcddvds 11564 dfgcd2 11614 txbasval 12347 cnmpt12 12367 cnmpt22 12374 |
Copyright terms: Public domain | W3C validator |