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  2931  brab2a  4754  brab2ga  4779  elovmpt2  6080  eqop2  6179  iscard  7624  iscard2  7625  elnnnn0  10023  elfzo2  10894  bitsval  12631  1nprm  12779  funcpropd  13790  isfull  13800  isfth  13804  ismhm  14433  isghm  14699  ghmpropd  14736  isga  14761  oppgcntz  14853  gexdvdsi  14910  isrhm  15517  abvpropd  15623  islmhm  15800  dfprm2  16463  prmirred  16464  elocv  16584  isobs  16636  iscn2  16984  iscnp2  16985  elflim2  17675  isfcls  17720  isnghm  18248  isnmhm  18271  0plef  19043  elply  19593  dchrelbas4  20498  isph  21416  abfmpunirn  23231  iscvm  23805  ceqsrexv2  24093  islocfin  26399  biadan2OLD  26436  eldiophb  26939  eldioph3b  26947  eldioph4b  26997  issdrg  27608  nb3grapr  28289
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