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  1192  3biant1d  1392  drex1  1847  elrab3t  2972  eldifvsn  3826  bnd2  4286  opbrop  4829  opelresi  5049  funcnv3  5418  fnssresb  5470  dff1o5  5623  fneqeql2  5787  fnniniseg2  5801  dffo3  5824  fmptco  5843  fnressn  5870  fconst4m  5904  riota2df  6025  eloprabga  6140  suppimacnvfn  6446  mptsuppd  6456  suppssrst  6461  suppssrgst  6462  frecabcl  6630  mptelixpg  6969  exmidfodomrlemreseldju  7503  enq0breq  7751  genpassl  7839  genpassu  7840  elnnnn0  9539  peano2z  9613  znnsub  9629  znn0sub  9643  uzin  9887  nn01to3  9949  rpnegap  10019  negelrp  10020  xsubge0  10214  divelunit  10335  elfz5  10351  uzsplit  10426  elfzonelfzo  10575  infssuzex  10593  adddivflid  10652  divfl0  10656  hashfibclem  11206  swrdspsleq  11359  2shfti  11516  rexuz3  11675  clim2c  11969  fisumss  12078  bitsmod  12642  bitscmp  12644  bezoutlemmain  12694  nninfctlemfo  12736  dvdsfi  12936  pc2dvds  13028  1arith  13065  xpsfrnel  13557  xpsfrnel2  13559  ghmeqker  13988  lsslss  14529  zndvds  14797  znleval2  14802  eltg3  14922  lmbrf  15080  cnrest2  15101  cnptoprest  15104  cnptoprest2  15105  ismet2  15219  elbl2ps  15257  elbl2  15258  xblpnfps  15263  xblpnf  15264  bdxmet  15366  metcn  15379  cnbl0  15399  cnblcld  15400  mulc1cncf  15454  ellimc3apf  15525  pilem1  15644  wilthlem1  15848  lgsdilem  15900  lgsne0  15911  lgsabs1  15912  lgsquadlem1  15950  lgsquadlem2  15951  isclwwlknx  16411  clwwlkn1  16413