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

Theorem anbi12ci 730
Description: Variant of anbi12i 729 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 729 . 2 ((𝜑𝜒) ↔ (𝜓𝜃))
4 ancom 465 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
53, 4bitri 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:  eu1  2498  compleq  3714  opelopabsbALT  4899  cnvpo  5576  f1cnvcnv  6007  cnvimadfsn  7169  oppcsect  16210  odupos  16907  oppr1  18406  ordtrest2  20766  3cyclfrgrarn1  26333  mdsldmd1i  28368  oduprs  28781  ordtrest2NEW  29091  cnvco1  30697  cnvco2  30698  pocnv  30701  dfiota3  30994  brcup  31010  brcap  31011  dfrdg4  31022  trer  31274  bj-ssbequ2  31626  dffrege115  37086  3cyclfrgrrn1  41447  frgr2wwlkeqm  41488
  Copyright terms: Public domain W3C validator