Theorem biadan2 648

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

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  3191  brab2a  4887  brab2ga  4913  elovmpt2  6519  eqop2  6839  iscard  8414  iscard2  8415  elnnnn0  10920  elfzo2  11930  bitsval  14409  1nprm  14641  funcpropd  15817  isfull  15827  isfth  15831  ismhm  16596  isghm  16895  ghmpropd  16932  isga  16957  oppgcntz  17027  gexdvdsi  17246  isrhm  17961  abvpropd  18082  islmhm  18262  dfprm2  19077  prmirred  19078  elocv  19243  isobs  19295  iscn2  20266  iscnp2  20267  islocfin  20544  elflim2  20991  isfcls  21036  isnghm  21740  isnghmOLD  21758  isnmhm  21779  0plef  22642  elply  23161  dchrelbas4  24183  nb3grapr  25193  isph  26475  abfmpunirn  28263  iscvm  29994  sscoid  30692  eldiophb  35611  eldioph3b  35619  eldioph4b  35666  issdrg  36075  brfvrcld2  36296  nb3grpr  39466  ismgmhm  39887  isrnghm  39996