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  2958  bnd2  4257  opbrop  4798  opelresi  5016  funcnv3  5383  fnssresb  5435  dff1o5  5583  fneqeql2  5746  fnniniseg2  5760  rexsupp  5761  dffo3  5784  fmptco  5803  fnressn  5829  fconst4m  5863  riota2df  5982  eloprabga  6097  frecabcl  6551  mptelixpg  6889  exmidfodomrlemreseldju  7389  enq0breq  7634  genpassl  7722  genpassu  7723  elnnnn0  9423  peano2z  9493  znnsub  9509  znn0sub  9523  uzin  9767  nn01to3  9824  rpnegap  9894  negelrp  9895  xsubge0  10089  divelunit  10210  elfz5  10225  uzsplit  10300  elfzonelfzo  10448  infssuzex  10465  adddivflid  10524  divfl0  10528  swrdspsleq  11214  2shfti  11357  rexuz3  11516  clim2c  11810  fisumss  11918  bitsmod  12482  bitscmp  12484  bezoutlemmain  12534  nninfctlemfo  12576  dvdsfi  12776  pc2dvds  12868  1arith  12905  xpsfrnel  13392  xpsfrnel2  13394  ghmeqker  13823  lsslss  14360  zndvds  14628  znleval2  14633  eltg3  14746  lmbrf  14904  cnrest2  14925  cnptoprest  14928  cnptoprest2  14929  ismet2  15043  elbl2ps  15081  elbl2  15082  xblpnfps  15087  xblpnf  15088  bdxmet  15190  metcn  15203  cnbl0  15223  cnblcld  15224  mulc1cncf  15278  ellimc3apf  15349  pilem1  15468  wilthlem1  15669  lgsdilem  15721  lgsne0  15732  lgsabs1  15733  lgsquadlem1  15771  lgsquadlem2  15772