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  1191  3biant1d  1391  drex1  1846  elrab3t  2961  bnd2  4263  opbrop  4805  opelresi  5024  funcnv3  5392  fnssresb  5444  dff1o5  5592  fneqeql2  5756  fnniniseg2  5770  rexsupp  5771  dffo3  5794  fmptco  5813  fnressn  5840  fconst4m  5874  riota2df  5993  eloprabga  6108  frecabcl  6565  mptelixpg  6903  exmidfodomrlemreseldju  7411  enq0breq  7656  genpassl  7744  genpassu  7745  elnnnn0  9445  peano2z  9515  znnsub  9531  znn0sub  9545  uzin  9789  nn01to3  9851  rpnegap  9921  negelrp  9922  xsubge0  10116  divelunit  10237  elfz5  10252  uzsplit  10327  elfzonelfzo  10476  infssuzex  10494  adddivflid  10553  divfl0  10557  swrdspsleq  11252  2shfti  11409  rexuz3  11568  clim2c  11862  fisumss  11971  bitsmod  12535  bitscmp  12537  bezoutlemmain  12587  nninfctlemfo  12629  dvdsfi  12829  pc2dvds  12921  1arith  12958  xpsfrnel  13445  xpsfrnel2  13447  ghmeqker  13876  lsslss  14414  zndvds  14682  znleval2  14687  eltg3  14800  lmbrf  14958  cnrest2  14979  cnptoprest  14982  cnptoprest2  14983  ismet2  15097  elbl2ps  15135  elbl2  15136  xblpnfps  15141  xblpnf  15142  bdxmet  15244  metcn  15257  cnbl0  15277  cnblcld  15278  mulc1cncf  15332  ellimc3apf  15403  pilem1  15522  wilthlem1  15723  lgsdilem  15775  lgsne0  15786  lgsabs1  15787  lgsquadlem1  15825  lgsquadlem2  15826  isclwwlknx  16286  clwwlkn1  16288