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

Theorem anbi12ci 681
Description: Variant of anbi12i 680 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 680 . 2  |-  ( (
ph  /\  ch )  <->  ( ps  /\  th )
)
4 ancom 439 . 2  |-  ( ( ps  /\  th )  <->  ( th  /\  ps )
)
53, 4bitri 242 1  |-  ( (
ph  /\  ch )  <->  ( th  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  opelopabsbOLD  4466  cnvpo  5413  f1cnvcnv  5650  oppcsect  14004  odupos  14567  oppr1  15744  ordtrest2  17273  mdsldmd1i  23839  cnvco1  25388  cnvco2  25389  dfiota3  25773  brcup  25789  brcap  25790  dfrdg4  25800  tfrqfree  25801  trer  26333  3cyclfrgrarn1  28476
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 179  df-an 362
  Copyright terms: Public domain W3C validator