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  1167  drex1  1812  elrab3t  2919  bnd2  4207  opbrop  4743  opelresi  4958  funcnv3  5321  fnssresb  5373  dff1o5  5516  fneqeql2  5674  fnniniseg2  5688  rexsupp  5689  dffo3  5712  fmptco  5731  fnressn  5751  fconst4m  5785  riota2df  5901  eloprabga  6013  frecabcl  6466  mptelixpg  6802  exmidfodomrlemreseldju  7281  enq0breq  7522  genpassl  7610  genpassu  7611  elnnnn0  9311  peano2z  9381  znnsub  9396  znn0sub  9410  uzin  9653  nn01to3  9710  rpnegap  9780  negelrp  9781  xsubge0  9975  divelunit  10096  elfz5  10111  uzsplit  10186  elfzonelfzo  10325  infssuzex  10342  adddivflid  10401  divfl0  10405  2shfti  11015  rexuz3  11174  clim2c  11468  fisumss  11576  bitsmod  12140  bitscmp  12142  bezoutlemmain  12192  nninfctlemfo  12234  dvdsfi  12434  pc2dvds  12526  1arith  12563  xpsfrnel  13048  xpsfrnel2  13050  ghmeqker  13479  lsslss  14015  zndvds  14283  znleval2  14288  eltg3  14401  lmbrf  14559  cnrest2  14580  cnptoprest  14583  cnptoprest2  14584  ismet2  14698  elbl2ps  14736  elbl2  14737  xblpnfps  14742  xblpnf  14743  bdxmet  14845  metcn  14858  cnbl0  14878  cnblcld  14879  mulc1cncf  14933  ellimc3apf  15004  pilem1  15123  wilthlem1  15324  lgsdilem  15376  lgsne0  15387  lgsabs1  15388  lgsquadlem1  15426  lgsquadlem2  15427