Theorem biantrurd 303

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 299	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpbirand  438  3anibar  1150  drex1  1771  elrab3t  2843  bnd2  4105  opbrop  4626  opelresi  4838  funcnv3  5193  fnssresb  5243  dff1o5  5384  fneqeql2  5537  fnniniseg2  5551  rexsupp  5552  dffo3  5575  fmptco  5594  fnressn  5614  fconst4m  5648  riota2df  5758  eloprabga  5866  frecabcl  6304  mptelixpg  6636  exmidfodomrlemreseldju  7073  enq0breq  7268  genpassl  7356  genpassu  7357  elnnnn0  9044  peano2z  9114  znnsub  9129  znn0sub  9143  uzin  9382  nn01to3  9436  rpnegap  9503  negelrp  9504  xsubge0  9694  divelunit  9815  elfz5  9829  uzsplit  9903  elfzonelfzo  10038  adddivflid  10096  divfl0  10100  2shfti  10635  rexuz3  10794  clim2c  11085  fisumss  11193  infssuzex  11678  bezoutlemmain  11722  eltg3  12265  lmbrf  12423  cnrest2  12444  cnptoprest  12447  cnptoprest2  12448  ismet2  12562  elbl2ps  12600  elbl2  12601  xblpnfps  12606  xblpnf  12607  bdxmet  12709  metcn  12722  cnbl0  12742  cnblcld  12743  mulc1cncf  12784  ellimc3apf  12837  pilem1  12908