![]() |
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 453 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏))) |
3 | bi2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂)) | |
4 | 3 | anbi2d 452 | . 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
5 | 2, 4 | sylan9bb 450 | 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 572 rspc2gv 2722 ralprg 3467 raltpg 3469 prssg 3568 prsspwg 3570 opelopab2a 4056 opelxp 4430 eqrel 4485 eqrelrel 4497 brcog 4561 dff13 5487 resoprab2 5677 ovig 5701 dfoprab4f 5898 f1o2ndf1 5928 eroveu 6313 th3qlem1 6324 th3qlem2 6325 th3q 6327 oviec 6328 endisj 6470 dfplpq2 6816 dfmpq2 6817 ordpipqqs 6836 enq0enq 6893 mulnnnq0 6912 ltsrprg 7196 axcnre 7319 axmulgt0 7461 addltmul 8544 ltxr 9141 sumsqeq0 9870 dvds2lem 10588 opoe 10675 omoe 10676 opeo 10677 omeo 10678 gcddvds 10735 dfgcd2 10783 |
Copyright terms: Public domain | W3C validator |