Theorem biantrurd 726

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 725	. 2 |- (ph -> (ch <-> (ch /\ ps)))
3		ancom 435	. 2 |- ((ch /\ ps) <-> (ps /\ ch))
4	2, 3	syl6bb 535	1 |- (ph -> (ch <-> (ps /\ ch)))

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

This theorem is referenced by:  sbcgf 1982  reldisj 2309  reuxfr 2899  opbrop 3233  funcnv3 3550  fnssresb 3591  dffo3 3810  fconst4 3842  eloprabg 3998  mapxpen 4481  bnd2 4704  kmlem2 4746  iscard2 4834  supxrre 6038  supxrre1 6048  elnnnn0 6127  znnsubt 6132  znn0subt 6133  icounlem 6353  elfz5t 6414  cau3i 6859  dffsum 6944  qdensere 7701  metgt0 7772  lmbrf 7882  lmbrf2 7883  iscauf 7891  iscau5 7893  lmclimnn 7915  nmo0 8396  pilem1 8609  pilem3 8611  axgroth2 8717  h2hcau 8788  h2hlm 8789  ch0psst 9307  pjnorm2t 9612  dfbdop2 9726  leopt 9994  atcv0eq 10243  elo 10381

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