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  4824  elrnmpt1  5010  fliftf  5974  elxp7  6366  eroveu  6862  sbthlemi5  7233  sbthlemi6  7234  elfi2  7261  sspw1or2  7497  reapltxor  8868  divap0b  8962  nnle1eq1  9266  nn0le0eq0  9529  nn0lt10b  9664  ioopos  10289  xrmaxiflemcom  11942  fz1f1o  12068  nndivdvds  12490  dvdsmultr2  12527  bitsmod  12650  pcmpt  13049  pcmpt2  13050  resrhm2b  14417  lssle0  14569  discld  15050  cncnpi  15142  cnptoprest2  15154  lmss  15160  txcn  15189  isxmet2d  15262  xblss2  15319  bdxmet  15415  xmetxp  15421  cncfcdm  15496  lgsneg  15946  lgsdilem  15949  2lgslem1a  16010  clwwlknonel  16476  clwwlknun  16485  eupth2lem2dc  16503