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

Theorem biadan2 624
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 615 . 2  |-  ( ph  <->  ( ps  /\  ph )
)
3 biadan2.2 . . 3  |-  ( ps 
->  ( ph  <->  ch )
)
43pm5.32i 619 . 2  |-  ( ( ps  /\  ph )  <->  ( ps  /\  ch )
)
52, 4bitri 241 1  |-  ( ph  <->  ( ps  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  elab4g  3078  brab2a  4919  brab2ga  4943  elovmpt2  6283  eqop2  6382  iscard  7854  iscard2  7855  elnnnn0  10255  elfzo2  11135  bitsval  12928  1nprm  13076  funcpropd  14089  isfull  14099  isfth  14103  ismhm  14732  isghm  14998  ghmpropd  15035  isga  15060  oppgcntz  15152  gexdvdsi  15209  isrhm  15816  abvpropd  15922  islmhm  16095  dfprm2  16766  prmirred  16767  elocv  16887  isobs  16939  iscn2  17294  iscnp2  17295  elflim2  17988  isfcls  18033  isnghm  18749  isnmhm  18772  0plef  19556  elply  20106  dchrelbas4  21019  nb3grapr  21454  isph  22315  abfmpunirn  24056  iscvm  24938  sscoid  25750  islocfin  26367  eldiophb  26806  eldioph3b  26814  eldioph4b  26863  issdrg  27473
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 178  df-an 361
  Copyright terms: Public domain W3C validator