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

Theorem anbi12ci 680
Description: Variant of anbi12i 679 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 679 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 ancom 438 . 2  |-  ( ( ps  /\  th )  <->  ( th  /\  ps )
)
53, 4bitri 241 1  |-  ( (
ph  /\  ch )  <->  ( th  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  opelopabsbOLD  4431  cnvpo  5377  f1cnvcnv  5614  oppcsect  13962  odupos  14525  oppr1  15702  ordtrest2  17230  mdsldmd1i  23795  cnvco1  25339  cnvco2  25340  dfiota3  25684  dfrdg4  25711  tfrqfree  25712  trer  26217  3cyclfrgrarn1  28124
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 178  df-an 361
  Copyright terms: Public domain W3C validator