![]() |
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 465 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜏))) |
3 | bi2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂)) | |
4 | 3 | anbi2d 464 | . 2 ⊢ (𝜃 → ((𝜒 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
5 | 2, 4 | sylan9bb 462 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: bi2anan9r 607 rspc2gv 2868 ralprg 3658 raltpg 3660 prssg 3764 prsspwg 3767 opelopab2a 4283 opelxp 4674 eqrel 4733 eqrelrel 4745 brcog 4812 dff13 5790 resoprab2 5993 ovig 6018 dfoprab4f 6218 f1o2ndf1 6253 eroveu 6652 th3qlem1 6663 th3qlem2 6664 th3q 6666 oviec 6667 endisj 6850 exmidapne 7289 dfplpq2 7383 dfmpq2 7384 ordpipqqs 7403 enq0enq 7460 mulnnnq0 7479 ltsrprg 7776 axcnre 7910 axmulgt0 8059 addltmul 9185 ltxr 9805 sumsqeq0 10630 mul0inf 11281 dvds2lem 11842 opoe 11932 omoe 11933 opeo 11934 omeo 11935 gcddvds 11996 dfgcd2 12047 pcqmul 12335 xpsfrnel2 12822 eqgval 13162 txbasval 14227 cnmpt12 14247 cnmpt22 14254 2sqlem7 14929 |
Copyright terms: Public domain | W3C validator |