|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > anbi12ci | Structured version Visualization version GIF version | ||
| Description: Variant of anbi12i 628 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) | 
| Ref | Expression | 
|---|---|
| anbi12.1 | ⊢ (𝜑 ↔ 𝜓) | 
| anbi12.2 | ⊢ (𝜒 ↔ 𝜃) | 
| Ref | Expression | 
|---|---|
| anbi12ci | ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | anbi12.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 2 | anbi12.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
| 3 | 1, 2 | anbi12i 628 | . 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) | 
| 4 | 3 | biancomi 462 | 1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ 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: eu1 2609 compleq 4151 cnvpo 6306 f1cnvcnv 6812 fsplit 8143 cnvimadfsn 8198 oppcsect 17823 oduprs 18347 odupos 18374 oppr1 20351 ordtrest2 23213 wwlks2onsym 29979 3cyclfrgrrn1 30305 fusgr2wsp2nb 30354 mdsldmd1i 32351 isunit2 33245 ordtrest2NEW 33923 cnvco1 35760 cnvco2 35761 pocnv 35764 dfiota3 35925 brcup 35941 brcap 35942 trer 36318 bj-nnfnt 36742 bj-gabima 36942 undmrnresiss 43622 dffrege115 43996 | 
| Copyright terms: Public domain | W3C validator |