| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > bi2anan9r | Structured version Visualization version GIF version | ||
| Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.) |
| Ref | Expression |
|---|---|
| bi2an9.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| bi2an9.2 | ⊢ (𝜃 → (𝜏 ↔ 𝜂)) |
| Ref | Expression |
|---|---|
| bi2anan9r | ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bi2an9.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | bi2an9.2 | . . 3 ⊢ (𝜃 → (𝜏 ↔ 𝜂)) | |
| 3 | 1, 2 | bi2anan9 638 | . 2 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
| 4 | 3 | ancoms 458 | 1 ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: efrn2lp 5666 ltsosr 11134 seqf1olem2 14083 seqf1o 14084 pcval 16882 sltlpss 27945 uspgr2wlkeq 29664 satf0op 35382 fmlafvel 35390 fneval 36353 prtlem5 38861 prjspval 42613 rmydioph 43026 wepwsolem 43054 aomclem8 43073 sprsymrelfolem2 47480 |
| Copyright terms: Public domain | W3C validator |