Theorem biadan2 637

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 628	. 2 |- ( ph <-> ( ps /\ ph ) )
3		biadan2.2	. . 3 |- ( ps -> ( ph <-> ch ) )
4	3	pm5.32i 632	. 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  3107  brab2a  4884  brab2ga  4908  elovmpt2  6306  eqop2  6616  iscard  8141  iscard2  8142  elnnnn0  10619  elfzo2  11552  bitsval  13616  1nprm  13764  funcpropd  14806  isfull  14816  isfth  14820  ismhm  15462  isghm  15740  ghmpropd  15777  isga  15802  oppgcntz  15872  gexdvdsi  16075  isrhm  16801  abvpropd  16907  islmhm  17086  dfprm2  17877  prmirred  17878  dfprm2OLD  17880  prmirredOLD  17881  elocv  18052  isobs  18104  iscn2  18801  iscnp2  18802  elflim2  19496  isfcls  19541  isnghm  20261  isnmhm  20284  0plef  21109  elply  21622  dchrelbas4  22541  nb3grapr  23296  isph  24157  abfmpunirn  25902  iscvm  27078  sscoid  27873  islocfin  28493  eldiophb  29020  eldioph3b  29028  eldioph4b  29075  issdrg  29479