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

Theorem anbi12ci 679
Description: Variant of anbi12i 678 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
anbi12.1  |-  ( ph  <->  ps )
anbi12.2  |-  ( ch  <->  th )
Assertion
Ref Expression
anbi12ci  |-  ( (
ph  /\  ch )  <->  ( th  /\  ps )
)

Proof of Theorem anbi12ci
StepHypRef Expression
1 anbi12.1 . . 3  |-  ( ph  <->  ps )
2 anbi12.2 . . 3  |-  ( ch  <->  th )
31, 2anbi12i 678 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 ancom 437 . 2  |-  ( ( ps  /\  th )  <->  ( th  /\  ps )
)
53, 4bitri 240 1  |-  ( (
ph  /\  ch )  <->  ( th  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  opelopabsbOLD  4273  cnvpo  5213  f1cnvcnv  5445  oppcsect  13676  odupos  14239  oppr1  15416  ordtrest2  16934  mdsldmd1i  22911  cnvco1  24117  cnvco2  24118  dfiota3  24462  dfrdg4  24488  tfrqfree  24489  trer  26227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator