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  4751  elrnmpt1  4934  fliftf  5875  elxp7  6263  eroveu  6720  sbthlemi5  7070  sbthlemi6  7071  elfi2  7081  reapltxor  8669  divap0b  8763  nnle1eq1  9067  nn0le0eq0  9330  nn0lt10b  9460  ioopos  10079  xrmaxiflemcom  11604  fz1f1o  11730  nndivdvds  12151  dvdsmultr2  12188  bitsmod  12311  pcmpt  12710  pcmpt2  12711  resrhm2b  14055  lssle0  14178  discld  14652  cncnpi  14744  cnptoprest2  14756  lmss  14762  txcn  14791  isxmet2d  14864  xblss2  14921  bdxmet  15017  xmetxp  15023  cncfcdm  15098  lgsneg  15545  lgsdilem  15548  2lgslem1a  15609