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

Theorem anbi12ci 622
Description: Variant of anbi12i 621 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 621 . 2 ((𝜑𝜒) ↔ (𝜓𝜃))
4 ancom 453 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
53, 4bitri 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:  eu1  2662  compleq  3950  opelopabsbALT  5180  cnvpo  5892  f1cnvcnv  6325  fsplit  7519  cnvimadfsn  7541  oppcsect  16752  odupos  17450  oppr1  18950  ordtrest2  21337  wwlks2onsym  27248  3cyclfrgrrn1  27634  fusgr2wsp2nb  27683  mdsldmd1i  29715  oduprs  30172  ordtrest2NEW  30485  cnvco1  32163  cnvco2  32164  pocnv  32167  dfiota3  32543  brcup  32559  brcap  32560  trer  32823  bj-ssbequ2  33149  undmrnresiss  38693  dffrege115  39054
  Copyright terms: Public domain W3C validator