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

Theorem anbi12ci 629
Description: Variant of anbi12i 628 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 628 . 2 ((𝜑𝜒) ↔ (𝜓𝜃))
43biancomi 462 1 ((𝜑𝜒) ↔ (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  eu1  2609  compleq  4151  cnvpo  6306  f1cnvcnv  6812  fsplit  8143  cnvimadfsn  8198  oppcsect  17823  oduprs  18347  odupos  18374  oppr1  20351  ordtrest2  23213  wwlks2onsym  29979  3cyclfrgrrn1  30305  fusgr2wsp2nb  30354  mdsldmd1i  32351  isunit2  33245  ordtrest2NEW  33923  cnvco1  35760  cnvco2  35761  pocnv  35764  dfiota3  35925  brcup  35941  brcap  35942  trer  36318  bj-nnfnt  36742  bj-gabima  36942  undmrnresiss  43622  dffrege115  43996
  Copyright terms: Public domain W3C validator