| 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 2889 ralprg 3684 raltpg 3686 prssg 3790 prsspwg 3793 opelopab2a 4311 opelxp 4705 eqrel 4764 eqrelrel 4776 brcog 4845 dff13 5837 resoprab2 6042 ovig 6067 dfoprab4f 6279 f1o2ndf1 6314 eroveu 6713 th3qlem1 6724 th3qlem2 6725 th3q 6727 oviec 6728 endisj 6919 exmidapne 7372 dfplpq2 7467 dfmpq2 7468 ordpipqqs 7487 enq0enq 7544 mulnnnq0 7563 ltsrprg 7860 axcnre 7994 axmulgt0 8144 addltmul 9274 ltxr 9897 sumsqeq0 10763 ccat0 11052 mul0inf 11552 dvds2lem 12114 opoe 12206 omoe 12207 opeo 12208 omeo 12209 gcddvds 12284 dfgcd2 12335 pcqmul 12626 xpsfrnel2 13178 eqgval 13559 txbasval 14739 cnmpt12 14759 cnmpt22 14766 lgsquadlem3 15556 lgsquad 15557 2sqlem7 15598 |
| Copyright terms: Public domain | W3C validator |