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

Theorem anbi12ci 698
Description: Variant of anbi12i 697 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 697 . 2
4 ancom 450 . 2
53, 4bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  eu1  2327  opelopabsbALT  4761  cnvpo  5550  f1cnvcnv  5794  cnvimadfsn  6927  oppcsect  15168  odupos  15765  oppr1  17283  ordtrest2  19705  3cyclfrgrarn1  25012  mdsldmd1i  27250  oduprs  27644  ordtrest2NEW  27905  cnvco1  29189  cnvco2  29190  pocnv  29193  dfiota3  29573  brcup  29589  brcap  29590  dfrdg4  29600  tfrqfree  29601  trer  30134
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 185  df-an 371
  Copyright terms: Public domain W3C validator