Theorem biadan2 640

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 631	. 2 |- ( ph <-> ( ps /\ ph ) )
3		biadan2.2	. . 3 |- ( ps -> ( ph <-> ch ) )
4	3	pm5.32i 635	. 2 |- ( ( ps /\ ph ) <-> ( ps /\ ch ) )
5	2, 4	bitri 249	1 |- ( ph <-> ( ps /\ ch ) )

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

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 369

This theorem is referenced by:  elab4g  3175  brab2a  4963  brab2ga  4989  elovmpt2  6419  eqop2  6740  iscard  8269  iscard2  8270  elnnnn0  10756  elfzo2  11725  bitsval  14076  1nprm  14224  funcpropd  15306  isfull  15316  isfth  15320  ismhm  16085  isghm  16384  ghmpropd  16421  isga  16446  oppgcntz  16516  gexdvdsi  16720  isrhm  17483  abvpropd  17604  islmhm  17786  dfprm2  18624  prmirred  18625  elocv  18790  isobs  18842  iscn2  19825  iscnp2  19826  islocfin  20103  elflim2  20550  isfcls  20595  isnghm  21315  isnmhm  21338  0plef  22164  elply  22677  dchrelbas4  23635  nb3grapr  24574  isph  25854  abfmpunirn  27630  iscvm  28893  sscoid  29716  eldiophb  30855  eldioph3b  30863  eldioph4b  30910  issdrg  31314  ismgmhm  32789  isrnghm  32898