Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  anbi2ci Structured version   Visualization version   GIF version

Theorem anbi2ci 627
 Description: Variant of anbi2i 625 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Hypothesis
Ref Expression
anbi.1 (𝜑𝜓)
Assertion
Ref Expression
anbi2ci ((𝜑𝜒) ↔ (𝜒𝜓))

Proof of Theorem anbi2ci
StepHypRef Expression
1 anbi.1 . . 3 (𝜑𝜓)
21anbi1i 626 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
32biancomi 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  1070  clabel  2934  difin0ss  4285  disjxun  5032  elidinxp  5882  cnvresima  6058  ordpwsuc  7523  supmo  8918  infmo  8961  kmlem3  9581  cfval2  9689  eqger  18343  gaorber  18451  opprunit  19428  xmeter  23081  iscvsp  23774  usgr2pth0  27598  elold  33530  bj-dfnnf2  34332  funALTVfun  36242  clsk1indlem4  40918  alimp-no-surprise  45475
 Copyright terms: Public domain W3C validator