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 438 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏))) |
3 | bi2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂)) | |
4 | 3 | anbi2d 437 | . 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
5 | 2, 4 | sylan9bb 435 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bi2anan9r 539 ralprg 3421 raltpg 3423 prssg 3521 prsspwg 3523 opelopab2a 4002 opelxp 4374 eqrel 4429 eqrelrel 4441 brcog 4502 dff13 5407 resoprab2 5598 ovig 5622 dfoprab4f 5819 f1o2ndf1 5849 eroveu 6197 th3qlem1 6208 th3qlem2 6209 th3q 6211 oviec 6212 endisj 6298 dfplpq2 6452 dfmpq2 6453 ordpipqqs 6472 enq0enq 6529 mulnnnq0 6548 ltsrprg 6832 axcnre 6955 axmulgt0 7091 addltmul 8161 ltxr 8695 sumsqeq0 9332 |
Copyright terms: Public domain | W3C validator |