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  1809  elrab3t  2916  bnd2  4203  opbrop  4739  opelresi  4954  funcnv3  5317  fnssresb  5367  dff1o5  5510  fneqeql2  5668  fnniniseg2  5682  rexsupp  5683  dffo3  5706  fmptco  5725  fnressn  5745  fconst4m  5779  riota2df  5895  eloprabga  6006  frecabcl  6454  mptelixpg  6790  exmidfodomrlemreseldju  7262  enq0breq  7498  genpassl  7586  genpassu  7587  elnnnn0  9286  peano2z  9356  znnsub  9371  znn0sub  9385  uzin  9628  nn01to3  9685  rpnegap  9755  negelrp  9756  xsubge0  9950  divelunit  10071  elfz5  10086  uzsplit  10161  elfzonelfzo  10300  adddivflid  10364  divfl0  10368  2shfti  10978  rexuz3  11137  clim2c  11430  fisumss  11538  infssuzex  12089  bezoutlemmain  12138  nninfctlemfo  12180  pc2dvds  12471  1arith  12508  xpsfrnel  12930  xpsfrnel2  12932  ghmeqker  13344  lsslss  13880  zndvds  14148  znleval2  14153  eltg3  14236  lmbrf  14394  cnrest2  14415  cnptoprest  14418  cnptoprest2  14419  ismet2  14533  elbl2ps  14571  elbl2  14572  xblpnfps  14577  xblpnf  14578  bdxmet  14680  metcn  14693  cnbl0  14713  cnblcld  14714  mulc1cncf  14768  ellimc3apf  14839  pilem1  14955  wilthlem1  15153  lgsdilem  15184  lgsne0  15195  lgsabs1  15196  lgsquadlem1  15234  lgsquadlem2  15235