Theorem biantrurd 731

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

Hypothesis

Ref	Expression
biantrud.1	⊢ (φ → ψ)

Assertion

Ref	Expression
biantrurd	⊢ (φ → (χ ↔ (ψ ⋀ χ)))

Proof of Theorem biantrurd

Step	Hyp	Ref	Expression
1		biantrud.1	. . 3 ⊢ (φ → ψ)
2	1	biantrud 730	. 2 ⊢ (φ → (χ ↔ (χ ⋀ ψ)))
3		ancom 438	. 2 ⊢ ((χ ⋀ ψ) ↔ (ψ ⋀ χ))
4	2, 3	syl6bb 539	1 ⊢ (φ → (χ ↔ (ψ ⋀ χ)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  sbcgf 1996  reldisj 2325  reuxfr 2920  opbrop 3254  funcnv3 3574  fnssresb 3615  dffo3 3835  fconst4 3867  eloprabg 4023  mapxpen 4515  bnd2 4741  kmlem2 4783  iscard2 4874  supxrre 6115  supxrre1 6125  elnnnn0 6204  znnsub 6209  znn0sub 6210  icounlem 6380  elfz5 6442  cau3ii 6946  dffsum 7030  qdensere 7777  metgt0 7846  lmbrf 7956  lmbrf2 7957  iscauf 7965  iscau5 7967  iscaunns 7970  lmclimnn 7990  nmo0 8476  pilem1 8695  pilem3 8697  axgroth2 8802  h2hcau 8873  h2hlm 8874  ch0pss 9393  pjnorm2 9696  dfbdop2 9810  leop 10080  atcv0eq 10331  elo 10469  eltids 10504

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