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  3biant1d  1366  drex1  1820  elrab3t  2927  bnd2  4216  opbrop  4753  opelresi  4969  funcnv3  5335  fnssresb  5387  dff1o5  5530  fneqeql2  5688  fnniniseg2  5702  rexsupp  5703  dffo3  5726  fmptco  5745  fnressn  5769  fconst4m  5803  riota2df  5919  eloprabga  6031  frecabcl  6484  mptelixpg  6820  exmidfodomrlemreseldju  7307  enq0breq  7548  genpassl  7636  genpassu  7637  elnnnn0  9337  peano2z  9407  znnsub  9423  znn0sub  9437  uzin  9680  nn01to3  9737  rpnegap  9807  negelrp  9808  xsubge0  10002  divelunit  10123  elfz5  10138  uzsplit  10213  elfzonelfzo  10357  infssuzex  10374  adddivflid  10433  divfl0  10437  2shfti  11084  rexuz3  11243  clim2c  11537  fisumss  11645  bitsmod  12209  bitscmp  12211  bezoutlemmain  12261  nninfctlemfo  12303  dvdsfi  12503  pc2dvds  12595  1arith  12632  xpsfrnel  13118  xpsfrnel2  13120  ghmeqker  13549  lsslss  14085  zndvds  14353  znleval2  14358  eltg3  14471  lmbrf  14629  cnrest2  14650  cnptoprest  14653  cnptoprest2  14654  ismet2  14768  elbl2ps  14806  elbl2  14807  xblpnfps  14812  xblpnf  14813  bdxmet  14915  metcn  14928  cnbl0  14948  cnblcld  14949  mulc1cncf  15003  ellimc3apf  15074  pilem1  15193  wilthlem1  15394  lgsdilem  15446  lgsne0  15457  lgsabs1  15458  lgsquadlem1  15496  lgsquadlem2  15497