Theorem biantrurd 299

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypothesis

Ref	Expression
biantrud.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
biantrurd	⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

Proof of Theorem biantrurd

Step	Hyp	Ref	Expression
1		biantrud.1	. 2 ⊢ (𝜑 → 𝜓)
2		ibar 295	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  3anibar  1106  drex1  1719  elrab3t  2748  bnd2  3947  opbrop  4437  opelresi  4641  funcnv3  4981  fnssresb  5031  dff1o5  5155  fneqeql2  5297  fnniniseg2  5311  rexsupp  5312  dffo3  5335  fmptco  5351  fnressn  5370  fconst4m  5402  riota2df  5508  eloprabga  5611  enq0breq  6626  genpassl  6714  genpassu  6715  elnnnn0  8331  peano2z  8387  znnsub  8402  znn0sub  8416  uzin  8651  nn01to3  8702  rpnegap  8766  divelunit  9024  elfz5  9037  uzsplit  9109  elfzonelfzo  9239  adddivflid  9294  divfl0  9298  2shfti  9719  rexuz3  9876  clim2c  10123  infssuzex  10345  bezoutlemmain  10387