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 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpbirand  445  3anibar  1196  3biant1d  1396  drex1  1851  elrab3t  2981  eldifvsn  3847  bnd2  4310  opbrop  4854  opelresi  5074  funcnv3  5443  fnssresb  5495  dff1o5  5648  fneqeql2  5818  fnniniseg2  5832  dffo3  5855  fmptco  5874  fnressn  5901  fconst4m  5935  riota2df  6060  eloprabga  6175  suppimacnvfn  6486  mptsuppd  6496  suppssrst  6501  suppssrgst  6502  frecabcl  6670  mptelixpg  7016  exmidfodomrlemreseldju  7552  enq0breq  7803  genpassl  7891  genpassu  7892  elnnnn0  9610  peano2z  9684  znnsub  9700  znn0sub  9714  uzin  9964  nn01to3  10026  rpnegap  10097  negelrp  10098  xsubge0  10293  divelunit  10414  elfz5  10430  uzsplit  10509  elfzonelfzo  10658  infssuzex  10676  adddivflid  10740  divfl0  10744  hashfibclem  11296  hashf1lem1  11299  swrdspsleq  11453  2shfti  11610  rexuz3  11770  clim2c  12066  fisumss  12175  bitsmod  12739  bitscmp  12741  bezoutlemmain  12791  nninfctlemfo  12833  dvdsfi  13037  pc2dvds  13129  1arith  13166  xpsfrnel  13714  xpsfrnel2  13716  ghmeqker  14123  lsslss  14767  zndvds  15033  znleval2  15038  eltg3  15207  lmbrf  15365  cnrest2  15386  cnptoprest  15389  cnptoprest2  15390  ismet2  15504  elbl2ps  15542  elbl2  15543  xblpnfps  15548  xblpnf  15549  bdxmet  15651  metcn  15664  cnbl0  15684  cnblcld  15685  mulc1cncf  15739  ellimc3apf  15810  pilem1  15930  wilthlem1  16151  bposlem1  16209  lgsdilem  16244  lgsne0  16255  lgsabs1  16256  lgsquadlem1  16294  lgsquadlem2  16295  isclwwlknx  16755  clwwlkn1  16757