MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biadan2 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  3022  brab2a  4860  brab2ga  4884  elovmpt2  6223  eqop2  6322  iscard  7788  iscard2  7789  elnnnn0  10188  elfzo2  11066  bitsval  12856  1nprm  13004  funcpropd  14017  isfull  14027  isfth  14031  ismhm  14660  isghm  14926  ghmpropd  14963  isga  14988  oppgcntz  15080  gexdvdsi  15137  isrhm  15744  abvpropd  15850  islmhm  16023  dfprm2  16690  prmirred  16691  elocv  16811  isobs  16863  iscn2  17217  iscnp2  17218  elflim2  17910  isfcls  17955  isnghm  18621  isnmhm  18644  0plef  19424  elply  19974  dchrelbas4  20887  nb3grapr  21321  isph  22164  abfmpunirn  23899  iscvm  24718  islocfin  26060  eldiophb  26499  eldioph3b  26507  eldioph4b  26556  issdrg  27167
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