Theorem biantrurd 727

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

Hypothesis

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

Assertion

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

Proof of Theorem biantrurd

Step	Hyp	Ref	Expression
1		biantrud.1	. . 3 |- (ph -> ps)
2	1	biantrud 726	. 2 |- (ph -> (ch <-> (ch /\ ps)))
3		ancom 435	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
4	2, 3	syl6bb 536	1 |- (ph -> (ch <-> (ps /\ ch)))

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

This theorem is referenced by:  sbcgf 1986  reldisj 2313  reuxfr 2904  opbrop 3238  funcnv3 3558  fnssresb 3599  dffo3 3819  fconst4 3851  eloprabg 4007  mapxpen 4495  bnd2 4724  kmlem2 4766  iscard2 4854  supxrre 6083  supxrre1 6093  elnnnn0 6172  znnsubt 6177  znn0subt 6178  icounlem 6412  elfz5t 6474  cau3i 6914  dffsum 6998  qdensere 7751  metgt0 7820  lmbrf 7930  lmbrf2 7931  iscauf 7939  iscau5 7941  iscaunns 7944  lmclimnn 7964  nmo0 8451  pilem1 8671  pilem3 8673  axgroth2 8778  h2hcau 8849  h2hlm 8850  ch0psst 9369  pjnorm2t 9672  dfbdop2 9786  leopt 10056  atcv0eq 10306  elo 10444

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