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  3236  brab2a  5039  brab2ga  5065  elovmpt2  6505  eqop2  6826  iscard  8359  iscard2  8360  elnnnn0  10845  elfzo2  11811  bitsval  13951  1nprm  14099  funcpropd  15143  isfull  15153  isfth  15157  ismhm  15842  isghm  16141  ghmpropd  16178  isga  16203  oppgcntz  16273  gexdvdsi  16477  isrhm  17244  abvpropd  17365  islmhm  17547  dfprm2  18397  prmirred  18398  dfprm2OLD  18400  prmirredOLD  18401  elocv  18572  isobs  18624  iscn2  19612  iscnp2  19613  islocfin  19891  elflim2  20338  isfcls  20383  isnghm  21103  isnmhm  21126  0plef  21952  elply  22465  dchrelbas4  23390  nb3grapr  24325  isph  25609  abfmpunirn  27362  iscvm  28577  sscoid  29538  eldiophb  30665  eldioph3b  30673  eldioph4b  30720  issdrg  31122  ismgmhm  32309  isrnghm  32416