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  1165  drex1  1798  elrab3t  2894  bnd2  4175  opbrop  4707  opelresi  4920  funcnv3  5280  fnssresb  5330  dff1o5  5472  fneqeql2  5628  fnniniseg2  5642  rexsupp  5643  dffo3  5666  fmptco  5685  fnressn  5705  fconst4m  5739  riota2df  5854  eloprabga  5965  frecabcl  6403  mptelixpg  6737  exmidfodomrlemreseldju  7202  enq0breq  7438  genpassl  7526  genpassu  7527  elnnnn0  9222  peano2z  9292  znnsub  9307  znn0sub  9321  uzin  9563  nn01to3  9620  rpnegap  9689  negelrp  9690  xsubge0  9884  divelunit  10005  elfz5  10020  uzsplit  10095  elfzonelfzo  10233  adddivflid  10295  divfl0  10299  2shfti  10843  rexuz3  11002  clim2c  11295  fisumss  11403  infssuzex  11953  bezoutlemmain  12002  pc2dvds  12332  1arith  12368  xpsfrnel  12770  xpsfrnel2  12772  lsslss  13506  eltg3  13745  lmbrf  13903  cnrest2  13924  cnptoprest  13927  cnptoprest2  13928  ismet2  14042  elbl2ps  14080  elbl2  14081  xblpnfps  14086  xblpnf  14087  bdxmet  14189  metcn  14202  cnbl0  14222  cnblcld  14223  mulc1cncf  14264  ellimc3apf  14317  pilem1  14388  lgsdilem  14616  lgsne0  14627  lgsabs1  14628