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  1165  drex1  1798  elrab3t  2894  bnd2  4175  opbrop  4707  opelresi  4920  funcnv3  5280  fnssresb  5330  dff1o5  5472  fneqeql2  5627  fnniniseg2  5641  rexsupp  5642  dffo3  5665  fmptco  5684  fnressn  5704  fconst4m  5738  riota2df  5853  eloprabga  5964  frecabcl  6402  mptelixpg  6736  exmidfodomrlemreseldju  7201  enq0breq  7437  genpassl  7525  genpassu  7526  elnnnn0  9221  peano2z  9291  znnsub  9306  znn0sub  9320  uzin  9562  nn01to3  9619  rpnegap  9688  negelrp  9689  xsubge0  9883  divelunit  10004  elfz5  10019  uzsplit  10094  elfzonelfzo  10232  adddivflid  10294  divfl0  10298  2shfti  10842  rexuz3  11001  clim2c  11294  fisumss  11402  infssuzex  11952  bezoutlemmain  12001  pc2dvds  12331  1arith  12367  xpsfrnel  12768  xpsfrnel2  12770  lsslss  13473  eltg3  13642  lmbrf  13800  cnrest2  13821  cnptoprest  13824  cnptoprest2  13825  ismet2  13939  elbl2ps  13977  elbl2  13978  xblpnfps  13983  xblpnf  13984  bdxmet  14086  metcn  14099  cnbl0  14119  cnblcld  14120  mulc1cncf  14161  ellimc3apf  14214  pilem1  14285  lgsdilem  14513  lgsne0  14524  lgsabs1  14525