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

Theorem anbi12ci 627
Description: Variant of anbi12i 626 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
anbi12.1 (𝜑𝜓)
anbi12.2 (𝜒𝜃)
Assertion
Ref Expression
anbi12ci ((𝜑𝜒) ↔ (𝜃𝜓))

Proof of Theorem anbi12ci
StepHypRef Expression
1 anbi12.1 . . 3 (𝜑𝜓)
2 anbi12.2 . . 3 (𝜒𝜃)
31, 2anbi12i 626 . 2 ((𝜑𝜒) ↔ (𝜓𝜃))
43biancomi 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:  eu1  2693  compleq  4128  opelopabsbALT  5413  cnvpo  6136  f1cnvcnv  6581  fsplit  7803  fsplitOLD  7804  cnvimadfsn  7830  oppcsect  17038  odupos  17735  oppr1  19304  ordtrest2  21731  wwlks2onsym  27654  3cyclfrgrrn1  27981  fusgr2wsp2nb  28030  mdsldmd1i  30025  oduprs  30560  ordtrest2NEW  31055  cnvco1  32882  cnvco2  32883  pocnv  32886  dfiota3  33271  brcup  33287  brcap  33288  trer  33551  bj-nnfnt  33956  undmrnresiss  39832  dffrege115  40192
  Copyright terms: Public domain W3C validator