Theorem biantrurd 305

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 301	. 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-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbirand  441  3anibar  1167  3biant1d  1366  drex1  1820  elrab3t  2927  bnd2  4216  opbrop  4752  opelresi  4967  funcnv3  5330  fnssresb  5382  dff1o5  5525  fneqeql2  5683  fnniniseg2  5697  rexsupp  5698  dffo3  5721  fmptco  5740  fnressn  5760  fconst4m  5794  riota2df  5910  eloprabga  6022  frecabcl  6475  mptelixpg  6811  exmidfodomrlemreseldju  7290  enq0breq  7531  genpassl  7619  genpassu  7620  elnnnn0  9320  peano2z  9390  znnsub  9406  znn0sub  9420  uzin  9663  nn01to3  9720  rpnegap  9790  negelrp  9791  xsubge0  9985  divelunit  10106  elfz5  10121  uzsplit  10196  elfzonelfzo  10340  infssuzex  10357  adddivflid  10416  divfl0  10420  2shfti  11061  rexuz3  11220  clim2c  11514  fisumss  11622  bitsmod  12186  bitscmp  12188  bezoutlemmain  12238  nninfctlemfo  12280  dvdsfi  12480  pc2dvds  12572  1arith  12609  xpsfrnel  13094  xpsfrnel2  13096  ghmeqker  13525  lsslss  14061  zndvds  14329  znleval2  14334  eltg3  14447  lmbrf  14605  cnrest2  14626  cnptoprest  14629  cnptoprest2  14630  ismet2  14744  elbl2ps  14782  elbl2  14783  xblpnfps  14788  xblpnf  14789  bdxmet  14891  metcn  14904  cnbl0  14924  cnblcld  14925  mulc1cncf  14979  ellimc3apf  15050  pilem1  15169  wilthlem1  15370  lgsdilem  15422  lgsne0  15433  lgsabs1  15434  lgsquadlem1  15472  lgsquadlem2  15473