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  1846  elrab3t  2962  eldifvsn  3810  bnd2  4269  opbrop  4811  opelresi  5030  funcnv3  5399  fnssresb  5451  dff1o5  5601  fneqeql2  5765  fnniniseg2  5779  dffo3  5802  fmptco  5821  fnressn  5848  fconst4m  5882  riota2df  6003  eloprabga  6118  suppimacnvfn  6424  mptsuppd  6434  suppssrst  6439  suppssrgst  6440  frecabcl  6608  mptelixpg  6946  exmidfodomrlemreseldju  7454  enq0breq  7699  genpassl  7787  genpassu  7788  elnnnn0  9487  peano2z  9559  znnsub  9575  znn0sub  9589  uzin  9833  nn01to3  9895  rpnegap  9965  negelrp  9966  xsubge0  10160  divelunit  10281  elfz5  10297  uzsplit  10372  elfzonelfzo  10521  infssuzex  10539  adddivflid  10598  divfl0  10602  swrdspsleq  11297  2shfti  11454  rexuz3  11613  clim2c  11907  fisumss  12016  bitsmod  12580  bitscmp  12582  bezoutlemmain  12632  nninfctlemfo  12674  dvdsfi  12874  pc2dvds  12966  1arith  13003  xpsfrnel  13490  xpsfrnel2  13492  ghmeqker  13921  lsslss  14460  zndvds  14728  znleval2  14733  eltg3  14851  lmbrf  15009  cnrest2  15030  cnptoprest  15033  cnptoprest2  15034  ismet2  15148  elbl2ps  15186  elbl2  15187  xblpnfps  15192  xblpnf  15193  bdxmet  15295  metcn  15308  cnbl0  15328  cnblcld  15329  mulc1cncf  15383  ellimc3apf  15454  pilem1  15573  wilthlem1  15777  lgsdilem  15829  lgsne0  15840  lgsabs1  15841  lgsquadlem1  15879  lgsquadlem2  15880  isclwwlknx  16340  clwwlkn1  16342