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

Theorem anbi2ci 619
Description: Variant of anbi2i 617 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 618 . 2 ((𝜑𝜒) ↔ (𝜓𝜒))
3 ancom 453 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
42, 3bitri 267 1 ((𝜑𝜒) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 385
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 199  df-an 386
This theorem is referenced by:  ifpn  1096  clabel  2924  difin0ss  4145  disjxun  4839  elidinxp  5665  cnvresima  5840  ordpwsuc  7247  supmo  8598  infmo  8641  kmlem3  9260  cfval2  9368  eqger  17953  gaorber  18049  opprunit  18973  xmeter  22562  iscvsp  23251  usgr2pth0  27010  bj-clabel  33270  clsk1indlem4  39111  alimp-no-surprise  43316
  Copyright terms: Public domain W3C validator