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

Theorem anbi12ci 734
Description: Variant of anbi12i 733 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 733 . 2 ((𝜑𝜒) ↔ (𝜓𝜃))
4 ancom 465 . 2 ((𝜓𝜃) ↔ (𝜃𝜓))
53, 4bitri 264 1 ((𝜑𝜒) ↔ (𝜃𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  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 197  df-an 385
This theorem is referenced by:  eu1  2539  compleq  3785  opelopabsbALT  5013  cnvpo  5711  f1cnvcnv  6147  cnvimadfsn  7349  oppcsect  16485  odupos  17182  oppr1  18680  ordtrest2  21056  wwlks2onsym  26924  3cyclfrgrrn1  27265  fusgr2wsp2nb  27314  mdsldmd1i  29318  oduprs  29784  ordtrest2NEW  30097  cnvco1  31775  cnvco2  31776  pocnv  31779  dfiota3  32155  brcup  32171  brcap  32172  dfrdg4  32183  trer  32435  bj-ssbequ2  32768  dffrege115  38589
  Copyright terms: Public domain W3C validator