Theorem biadan2 654

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  elab4g  3177  brab2a  4889  brab2ga  4915  elovmpt2  6533  eqop2  6853  iscard  8427  iscard2  8428  elnnnn0  10937  elfzo2  11950  bitsval  14476  1nprm  14708  funcpropd  15883  isfull  15893  isfth  15897  ismhm  16662  isghm  16961  ghmpropd  16998  isga  17023  oppgcntz  17093  gexdvdsi  17312  isrhm  18027  abvpropd  18148  islmhm  18328  dfprm2  19142  prmirred  19143  elocv  19308  isobs  19360  iscn2  20331  iscnp2  20332  islocfin  20609  elflim2  21057  isfcls  21102  isnghm  21806  isnghmOLD  21824  isnmhm  21845  0plef  22709  elply  23228  dchrelbas4  24250  nb3grapr  25260  isph  26544  abfmpunirn  28327  iscvm  30054  sscoid  30751  eldiophb  35670  eldioph3b  35678  eldioph4b  35725  issdrg  36134  brfvrcld2  36355  nb3grpr  39620  ismgmhm  40291  isrnghm  40400