![]() |
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 636 | . 2 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
4 | 3 | ancoms 458 | 1 ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ 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 206 df-an 396 |
This theorem is referenced by: efrn2lp 5658 ltsosr 11093 seqf1olem2 14013 seqf1o 14014 pcval 16782 sltlpss 27639 uspgr2wlkeq 29171 satf0op 34667 fmlafvel 34675 fneval 35541 prtlem5 38034 prjspval 41648 rmydioph 42056 wepwsolem 42087 aomclem8 42106 sprsymrelfolem2 46460 |
Copyright terms: Public domain | W3C validator |