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  4909  cnvpo  5590  f1cnvcnv  6022  cnvimadfsn  7191  oppcsect  16261  odupos  16958  oppr1  18457  ordtrest2  20818  3cyclfrgrarn1  26539  mdsldmd1i  28574  oduprs  28987  ordtrest2NEW  29297  cnvco1  30903  cnvco2  30904  pocnv  30907  dfiota3  31200  brcup  31216  brcap  31217  dfrdg4  31228  trer  31480  bj-ssbequ2  31832  dffrege115  37292  3cyclfrgrrn1  41455  frgr2wwlkeqm  41496
 Copyright terms: Public domain W3C validator