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

Theorem anbi2ci 624
Description: Variant of anbi2i 622 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 623 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
32biancomi 463 1 ((𝜑𝜒) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  ifpn  1066  clabel  2964  difin0ss  4332  disjxun  5061  elidinxp  5910  cnvresima  6085  ordpwsuc  7518  supmo  8905  infmo  8948  kmlem3  9567  cfval2  9671  eqger  18260  gaorber  18368  opprunit  19331  xmeter  22958  iscvsp  23647  usgr2pth0  27460  bj-dfnnf2  33950  funALTVfun  35798  clsk1indlem4  40259  alimp-no-surprise  44714
  Copyright terms: Public domain W3C validator