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

Theorem biadan2 647
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 638 . 2  |-  ( ph  <->  ( ps  /\  ph )
)
3 biadan2.2 . . 3  |-  ( ps 
->  ( ph  <->  ch )
)
43pm5.32i 642 . 2  |-  ( ( ps  /\  ph )  <->  ( ps  /\  ch )
)
52, 4bitri 253 1  |-  ( ph  <->  ( ps  /\  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  elab4g  3223  brab2a  4901  brab2ga  4927  elovmpt2  6526  eqop2  6846  iscard  8412  iscard2  8413  elnnnn0  10915  elfzo2  11925  bitsval  14390  1nprm  14622  funcpropd  15798  isfull  15808  isfth  15812  ismhm  16577  isghm  16876  ghmpropd  16913  isga  16938  oppgcntz  17008  gexdvdsi  17227  isrhm  17942  abvpropd  18063  islmhm  18243  dfprm2  19057  prmirred  19058  elocv  19223  isobs  19275  iscn2  20246  iscnp2  20247  islocfin  20524  elflim2  20971  isfcls  21016  isnghm  21720  isnghmOLD  21738  isnmhm  21759  0plef  22622  elply  23141  dchrelbas4  24163  nb3grapr  25173  isph  26455  abfmpunirn  28247  iscvm  29984  sscoid  30679  eldiophb  35562  eldioph3b  35570  eldioph4b  35617  issdrg  36027  brfvrcld2  36188  ismgmhm  39125  isrnghm  39234
  Copyright terms: Public domain W3C validator