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

Theorem anbi2ci 727
Description: Variant of anbi2i 725 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 726 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 ancom 464 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
42, 3bitri 262 1 ((𝜑𝜒) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382
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 195  df-an 384
This theorem is referenced by:  ifpn  1015  clabel  2735  difin0ss  3899  disjxun  4575  asymref  5417  ordpwsuc  6884  supmo  8218  infmo  8261  kmlem3  8834  cfval2  8942  eqger  17415  gaorber  17512  opprunit  18432  xmeter  21995  iscvsp  22683  bj-clabel  31764  clsk1indlem4  37145  usgr2pth0  40952  alimp-no-surprise  42278
  Copyright terms: Public domain W3C validator