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

Theorem biadan2 642
Description: Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.)
Hypotheses
Ref Expression
biadan2.1  |-  ( ph  ->  ps )
biadan2.2  |-  ( ps 
->  ( ph  <->  ch )
)
Assertion
Ref Expression
biadan2  |-  ( ph  <->  ( ps  /\  ch )
)

Proof of Theorem biadan2
StepHypRef Expression
1 biadan2.1 . . 3  |-  ( ph  ->  ps )
21pm4.71ri 633 . 2  |-  ( ph  <->  ( ps  /\  ph )
)
3 biadan2.2 . . 3  |-  ( ps 
->  ( ph  <->  ch )
)
43pm5.32i 637 . 2  |-  ( ( ps  /\  ph )  <->  ( ps  /\  ch )
)
52, 4bitri 249 1  |-  ( ph  <->  ( ps  /\  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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
This theorem is referenced by:  elab4g  3236  brab2a  5039  brab2ga  5065  elovmpt2  6505  eqop2  6826  iscard  8359  iscard2  8360  elnnnn0  10845  elfzo2  11811  bitsval  13951  1nprm  14099  funcpropd  15143  isfull  15153  isfth  15157  ismhm  15842  isghm  16141  ghmpropd  16178  isga  16203  oppgcntz  16273  gexdvdsi  16477  isrhm  17244  abvpropd  17365  islmhm  17547  dfprm2  18397  prmirred  18398  dfprm2OLD  18400  prmirredOLD  18401  elocv  18572  isobs  18624  iscn2  19612  iscnp2  19613  islocfin  19891  elflim2  20338  isfcls  20383  isnghm  21103  isnmhm  21126  0plef  21952  elply  22465  dchrelbas4  23390  nb3grapr  24325  isph  25609  abfmpunirn  27362  iscvm  28577  sscoid  29538  eldiophb  30665  eldioph3b  30673  eldioph4b  30720  issdrg  31122  ismgmhm  32309  isrnghm  32416
  Copyright terms: Public domain W3C validator