Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anbi2ci | Structured version Visualization version GIF version |
Description: Variant of anbi2i 626 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 627 | . 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
3 | 2 | biancomi 466 | 1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: ifpnOLD 1075 clabel 2882 difin0ss 4283 disjxun 5051 elidinxp 5911 cnvresima 6093 ordpwsuc 7594 supmo 9068 infmo 9111 kmlem3 9766 cfval2 9874 eqger 18594 gaorber 18702 opprunit 19679 xmeter 23331 iscvsp 24025 usgr2pth0 27852 elold 33790 bj-dfnnf2 34656 funALTVfun 36546 clsk1indlem4 41331 alimp-no-surprise 46156 |
Copyright terms: Public domain | W3C validator |