Theorem biantrud 725

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 516	1 |- (ph -> (ch <-> (ch /\ ps)))

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

This theorem is referenced by:  biantrurd 726  mapdom2 4480  cardval 4806  nn2get 5898  nnle1eq1t 5901  nn0le0eq0t 6074  ioopos 6334  cau2 6858  iscld4 7646  metxp 7786  shle0t 9304  lnopcon 9901  lnfncon 9928  mdsl2b 10187  dmdbr5at 10284  cdj3lem1 10295

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