Theorem biantrud 304

Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)

Hypothesis

Ref	Expression
biantrud.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem biantrud

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiran2d  442  posng  4791  elrnmpt1  4975  fliftf  5929  elxp7  6322  eroveu  6781  sbthlemi5  7139  sbthlemi6  7140  elfi2  7150  reapltxor  8747  divap0b  8841  nnle1eq1  9145  nn0le0eq0  9408  nn0lt10b  9538  ioopos  10158  xrmaxiflemcom  11776  fz1f1o  11902  nndivdvds  12323  dvdsmultr2  12360  bitsmod  12483  pcmpt  12882  pcmpt2  12883  resrhm2b  14229  lssle0  14352  discld  14826  cncnpi  14918  cnptoprest2  14930  lmss  14936  txcn  14965  isxmet2d  15038  xblss2  15095  bdxmet  15191  xmetxp  15197  cncfcdm  15272  lgsneg  15719  lgsdilem  15722  2lgslem1a  15783