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 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbirand  445  3anibar  1196  3biant1d  1396  drex1  1851  elrab3t  2981  eldifvsn  3847  bnd2  4312  opbrop  4856  opelresi  5076  funcnv3  5446  fnssresb  5498  dff1o5  5651  fneqeql2  5821  fnniniseg2  5835  dffo3  5858  fmptco  5877  fnressn  5904  fconst4m  5938  riota2df  6063  eloprabga  6178  suppimacnvfn  6490  mptsuppd  6500  suppssrst  6505  suppssrgst  6506  frecabcl  6674  mptelixpg  7020  relresfin  7268  exmidfodomrlemreseldju  7558  enq0breq  7809  genpassl  7897  genpassu  7898  elnnnn0  9617  peano2z  9691  znnsub  9707  znn0sub  9721  uzin  9971  nn01to3  10033  rpnegap  10104  negelrp  10105  xsubge0  10300  divelunit  10421  elfz5  10437  uzsplit  10516  elfzonelfzo  10665  infssuzex  10683  adddivflid  10748  divfl0  10752  hashfibclem  11304  hashf1lem1  11307  swrdspsleq  11461  2shfti  11618  rexuz3  11778  clim2c  12075  fisumss  12184  bitsmod  12748  bitscmp  12750  bezoutlemmain  12800  nninfctlemfo  12842  dvdsfi  13046  pc2dvds  13138  1arith  13175  xpsfrnel  13724  xpsfrnel2  13726  ghmeqker  14133  lsslss  14827  zndvds  15093  znleval2  15098  eltg3  15283  lmbrf  15441  cnrest2  15462  cnptoprest  15465  cnptoprest2  15466  ismet2  15580  elbl2ps  15618  elbl2  15619  xblpnfps  15624  xblpnf  15625  bdxmet  15727  metcn  15740  cnbl0  15760  cnblcld  15761  mulc1cncf  15815  ellimc3apf  15886  pilem1  16006  wilthlem1  16232  bposlem1  16311  lgsdilem  16351  lgsne0  16362  lgsabs1  16363  lgsquadlem1  16401  lgsquadlem2  16402  isclwwlknx  16862  clwwlkn1  16864