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  4206  opbrop  4742  opelresi  4957  funcnv3  5320  fnssresb  5370  dff1o5  5513  fneqeql2  5671  fnniniseg2  5685  rexsupp  5686  dffo3  5709  fmptco  5728  fnressn  5748  fconst4m  5782  riota2df  5898  eloprabga  6009  frecabcl  6457  mptelixpg  6793  exmidfodomrlemreseldju  7267  enq0breq  7503  genpassl  7591  genpassu  7592  elnnnn0  9292  peano2z  9362  znnsub  9377  znn0sub  9391  uzin  9634  nn01to3  9691  rpnegap  9761  negelrp  9762  xsubge0  9956  divelunit  10077  elfz5  10092  uzsplit  10167  elfzonelfzo  10306  infssuzex  10323  adddivflid  10382  divfl0  10386  2shfti  10996  rexuz3  11155  clim2c  11449  fisumss  11557  bezoutlemmain  12165  nninfctlemfo  12207  dvdsfi  12407  pc2dvds  12499  1arith  12536  xpsfrnel  12987  xpsfrnel2  12989  ghmeqker  13401  lsslss  13937  zndvds  14205  znleval2  14210  eltg3  14293  lmbrf  14451  cnrest2  14472  cnptoprest  14475  cnptoprest2  14476  ismet2  14590  elbl2ps  14628  elbl2  14629  xblpnfps  14634  xblpnf  14635  bdxmet  14737  metcn  14750  cnbl0  14770  cnblcld  14771  mulc1cncf  14825  ellimc3apf  14896  pilem1  15015  wilthlem1  15216  lgsdilem  15268  lgsne0  15279  lgsabs1  15280  lgsquadlem1  15318  lgsquadlem2  15319