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  1189  3biant1d  1389  drex1  1844  elrab3t  2959  bnd2  4261  opbrop  4803  opelresi  5022  funcnv3  5389  fnssresb  5441  dff1o5  5589  fneqeql2  5752  fnniniseg2  5766  rexsupp  5767  dffo3  5790  fmptco  5809  fnressn  5835  fconst4m  5869  riota2df  5988  eloprabga  6103  frecabcl  6560  mptelixpg  6898  exmidfodomrlemreseldju  7401  enq0breq  7646  genpassl  7734  genpassu  7735  elnnnn0  9435  peano2z  9505  znnsub  9521  znn0sub  9535  uzin  9779  nn01to3  9841  rpnegap  9911  negelrp  9912  xsubge0  10106  divelunit  10227  elfz5  10242  uzsplit  10317  elfzonelfzo  10465  infssuzex  10483  adddivflid  10542  divfl0  10546  swrdspsleq  11238  2shfti  11382  rexuz3  11541  clim2c  11835  fisumss  11943  bitsmod  12507  bitscmp  12509  bezoutlemmain  12559  nninfctlemfo  12601  dvdsfi  12801  pc2dvds  12893  1arith  12930  xpsfrnel  13417  xpsfrnel2  13419  ghmeqker  13848  lsslss  14385  zndvds  14653  znleval2  14658  eltg3  14771  lmbrf  14929  cnrest2  14950  cnptoprest  14953  cnptoprest2  14954  ismet2  15068  elbl2ps  15106  elbl2  15107  xblpnfps  15112  xblpnf  15113  bdxmet  15215  metcn  15228  cnbl0  15248  cnblcld  15249  mulc1cncf  15303  ellimc3apf  15374  pilem1  15493  wilthlem1  15694  lgsdilem  15746  lgsne0  15757  lgsabs1  15758  lgsquadlem1  15796  lgsquadlem2  15797  isclwwlknx  16211  clwwlkn1  16213