Theorem biadan2 642

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

Step	Hyp	Ref	Expression
1		biadan2.1	. . 3 |- ( ph -> ps )
2	1	pm4.71ri 633	. 2 |- ( ph <-> ( ps /\ ph ) )
3		biadan2.2	. . 3 |- ( ps -> ( ph <-> ch ) )
4	3	pm5.32i 637	. 2 |- ( ( ps /\ ph ) <-> ( ps /\ ch ) )
5	2, 4	bitri 249	1 |- ( ph <-> ( ps /\ ch ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  elab4g  3247  brab2a  5041  brab2ga  5066  elovmpt2  6495  eqop2  6815  iscard  8345  iscard2  8346  elnnnn0  10828  elfzo2  11789  bitsval  13922  1nprm  14070  funcpropd  15116  isfull  15126  isfth  15130  ismhm  15772  isghm  16055  ghmpropd  16092  isga  16117  oppgcntz  16187  gexdvdsi  16392  isrhm  17147  abvpropd  17267  islmhm  17449  dfprm2  18284  prmirred  18285  dfprm2OLD  18287  prmirredOLD  18288  elocv  18459  isobs  18511  iscn2  19498  iscnp2  19499  elflim2  20193  isfcls  20238  isnghm  20958  isnmhm  20981  0plef  21807  elply  22320  dchrelbas4  23239  nb3grapr  24115  isph  25399  abfmpunirn  27148  iscvm  28330  sscoid  29126  islocfin  29755  eldiophb  30281  eldioph3b  30289  eldioph4b  30336  issdrg  30740