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

Theorem biadan2 623
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 614 . 2  |-  ( ph  <->  ( ps  /\  ph )
)
3 biadan2.2 . . 3  |-  ( ps 
->  ( ph  <->  ch )
)
43pm5.32i 618 . 2  |-  ( ( ps  /\  ph )  <->  ( ps  /\  ch )
)
52, 4bitri 240 1  |-  ( ph  <->  ( ps  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  elab4g  2918  brab2a  4738  brab2ga  4763  elovmpt2  6064  eqop2  6163  iscard  7608  iscard2  7609  elnnnn0  10007  elfzo2  10878  bitsval  12615  1nprm  12763  funcpropd  13774  isfull  13784  isfth  13788  ismhm  14417  isghm  14683  ghmpropd  14720  isga  14745  oppgcntz  14837  gexdvdsi  14894  isrhm  15501  abvpropd  15607  islmhm  15784  dfprm2  16447  prmirred  16448  elocv  16568  isobs  16620  iscn2  16968  iscnp2  16969  elflim2  17659  isfcls  17704  isnghm  18232  isnmhm  18255  0plef  19027  elply  19577  dchrelbas4  20482  isph  21400  abfmpunirn  23216  iscvm  23790  ceqsrexv2  24078  islocfin  26296  biadan2OLD  26333  eldiophb  26836  eldioph3b  26844  eldioph4b  26894  issdrg  27505
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