Theorem biadan2 647

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 638	. 2 |- ( ph <-> ( ps /\ ph ) )
3		biadan2.2	. . 3 |- ( ps -> ( ph <-> ch ) )
4	3	pm5.32i 642	. 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  3223  brab2a  4901  brab2ga  4927  elovmpt2  6526  eqop2  6846  iscard  8412  iscard2  8413  elnnnn0  10915  elfzo2  11925  bitsval  14390  1nprm  14622  funcpropd  15798  isfull  15808  isfth  15812  ismhm  16577  isghm  16876  ghmpropd  16913  isga  16938  oppgcntz  17008  gexdvdsi  17227  isrhm  17942  abvpropd  18063  islmhm  18243  dfprm2  19057  prmirred  19058  elocv  19223  isobs  19275  iscn2  20246  iscnp2  20247  islocfin  20524  elflim2  20971  isfcls  21016  isnghm  21720  isnghmOLD  21738  isnmhm  21759  0plef  22622  elply  23141  dchrelbas4  24163  nb3grapr  25173  isph  26455  abfmpunirn  28247  iscvm  29984  sscoid  30679  eldiophb  35562  eldioph3b  35570  eldioph4b  35617  issdrg  36027  brfvrcld2  36188  ismgmhm  39125  isrnghm  39234