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

Theorem biadan2 654
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 645 . 2  |-  ( ph  <->  ( ps  /\  ph )
)
3 biadan2.2 . . 3  |-  ( ps 
->  ( ph  <->  ch )
)
43pm5.32i 649 . 2  |-  ( ( ps  /\  ph )  <->  ( ps  /\  ch )
)
52, 4bitri 257 1  |-  ( ph  <->  ( ps  /\  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  elab4g  3177  brab2a  4889  brab2ga  4915  elovmpt2  6533  eqop2  6853  iscard  8427  iscard2  8428  elnnnn0  10937  elfzo2  11950  bitsval  14476  1nprm  14708  funcpropd  15883  isfull  15893  isfth  15897  ismhm  16662  isghm  16961  ghmpropd  16998  isga  17023  oppgcntz  17093  gexdvdsi  17312  isrhm  18027  abvpropd  18148  islmhm  18328  dfprm2  19142  prmirred  19143  elocv  19308  isobs  19360  iscn2  20331  iscnp2  20332  islocfin  20609  elflim2  21057  isfcls  21102  isnghm  21806  isnghmOLD  21824  isnmhm  21845  0plef  22709  elply  23228  dchrelbas4  24250  nb3grapr  25260  isph  26544  abfmpunirn  28327  iscvm  30054  sscoid  30751  eldiophb  35670  eldioph3b  35678  eldioph4b  35725  issdrg  36134  brfvrcld2  36355  nb3grpr  39620  ismgmhm  40291  isrnghm  40400
  Copyright terms: Public domain W3C validator