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

Theorem anbi2ci 728
 Description: Variant of anbi2i 726 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 727 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 ancom 465 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
42, 3bitri 263 1 ((𝜑𝜒) ↔ (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  ifpn  1016  clabel  2736  difin0ss  3900  disjxun  4581  asymref  5431  ordpwsuc  6907  supmo  8241  infmo  8284  kmlem3  8857  cfval2  8965  eqger  17467  gaorber  17564  opprunit  18484  xmeter  22048  iscvsp  22736  bj-clabel  31971  clsk1indlem4  37362  usgr2pth0  40971  alimp-no-surprise  42336
 Copyright terms: Public domain W3C validator