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  5839  fconst4m  5873  riota2df  5992  eloprabga  6107  frecabcl  6564  mptelixpg  6902  exmidfodomrlemreseldju  7410  enq0breq  7655  genpassl  7743  genpassu  7744  elnnnn0  9444  peano2z  9514  znnsub  9530  znn0sub  9544  uzin  9788  nn01to3  9850  rpnegap  9920  negelrp  9921  xsubge0  10115  divelunit  10236  elfz5  10251  uzsplit  10326  elfzonelfzo  10474  infssuzex  10492  adddivflid  10551  divfl0  10555  swrdspsleq  11247  2shfti  11391  rexuz3  11550  clim2c  11844  fisumss  11952  bitsmod  12516  bitscmp  12518  bezoutlemmain  12568  nninfctlemfo  12610  dvdsfi  12810  pc2dvds  12902  1arith  12939  xpsfrnel  13426  xpsfrnel2  13428  ghmeqker  13857  lsslss  14394  zndvds  14662  znleval2  14667  eltg3  14780  lmbrf  14938  cnrest2  14959  cnptoprest  14962  cnptoprest2  14963  ismet2  15077  elbl2ps  15115  elbl2  15116  xblpnfps  15121  xblpnf  15122  bdxmet  15224  metcn  15237  cnbl0  15257  cnblcld  15258  mulc1cncf  15312  ellimc3apf  15383  pilem1  15502  wilthlem1  15703  lgsdilem  15755  lgsne0  15766  lgsabs1  15767  lgsquadlem1  15805  lgsquadlem2  15806  isclwwlknx  16266  clwwlkn1  16268