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  4352  cnvpo  5292  f1cnvcnv  5525  oppcsect  13769  odupos  14332  oppr1  15509  ordtrest2  17034  mdsldmd1i  23019  cnvco1  24675  cnvco2  24676  dfiota3  25020  dfrdg4  25047  tfrqfree  25048  trer  25551  3cyclfrgrarn1  27828
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