Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anbi2ci | Structured version Visualization version GIF version |
Description: Variant of anbi2i 730 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Ref | Expression |
---|---|
anbi.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
anbi2ci | ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anbi.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | anbi1i 731 | . 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
3 | ancom 466 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
4 | 2, 3 | bitri 264 | 1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 |
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 197 df-an 386 |
This theorem is referenced by: ifpn 1022 clabel 2749 difin0ss 3946 disjxun 4651 asymref 5512 ordpwsuc 7015 supmo 8358 infmo 8401 kmlem3 8974 cfval2 9082 eqger 17644 gaorber 17741 opprunit 18661 xmeter 22238 iscvsp 22928 usgr2pth0 26661 bj-clabel 32783 clsk1indlem4 38342 alimp-no-surprise 42527 |
Copyright terms: Public domain | W3C validator |