Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bi2anan9 | GIF 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 452 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏))) |
3 | bi2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂)) | |
4 | 3 | anbi2d 451 | . 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
5 | 2, 4 | sylan9bb 449 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: bi2anan9r 571 rspc2gv 2712 ralprg 3443 raltpg 3445 prssg 3542 prsspwg 3544 opelopab2a 4020 opelxp 4392 eqrel 4447 eqrelrel 4459 brcog 4520 dff13 5428 resoprab2 5618 ovig 5642 dfoprab4f 5839 f1o2ndf1 5869 eroveu 6220 th3qlem1 6231 th3qlem2 6232 th3q 6234 oviec 6235 endisj 6321 dfplpq2 6544 dfmpq2 6545 ordpipqqs 6564 enq0enq 6621 mulnnnq0 6640 ltsrprg 6924 axcnre 7047 axmulgt0 7184 addltmul 8267 ltxr 8849 sumsqeq0 9554 dvds2lem 10207 opoe 10295 omoe 10296 opeo 10297 omeo 10298 gcddvds 10355 dfgcd2 10403 |
Copyright terms: Public domain | W3C validator |