Theorem biantrud 726

Description: A wff is equivalent to its conjunction with truth.

Hypothesis

Ref	Expression
biantrud.1	|- (ph -> ps)

Assertion

Ref	Expression
biantrud	|- (ph -> (ch <-> (ch /\ ps)))

Proof of Theorem biantrud

Step	Hyp	Ref	Expression
1		biantrud.1	. . . 4 |- (ph -> ps)
2	1	anim2i 335	. . 3 |- ((ch /\ ph) -> (ch /\ ps))
3	2	expcom 374	. 2 |- (ph -> (ch -> (ch /\ ps)))
4		pm3.26 319	. 2 |- ((ch /\ ps) -> ch)
5	3, 4	impbid1 517	1 |- (ph -> (ch <-> (ch /\ ps)))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  biantrurd 727  mapdom2 4494  cardval 4826  nn2get 5942  nnle1eq1t 5945  nn0le0eq0t 6119  ioopos 6394  cau2 6913  iscld4 7696  metxp 7834  shle0t 9366  lnopcon 9963  lnfncon 9990  mdsl2b 10250  dmdbr5at 10349  cdj3lem1 10361

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain