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  437  3anibar  1149  drex1  1770  elrab3t  2834  bnd2  4092  opbrop  4613  opelresi  4825  funcnv3  5180  fnssresb  5230  dff1o5  5369  fneqeql2  5522  fnniniseg2  5536  rexsupp  5537  dffo3  5560  fmptco  5579  fnressn  5599  fconst4m  5633  riota2df  5743  eloprabga  5851  frecabcl  6289  mptelixpg  6621  exmidfodomrlemreseldju  7049  enq0breq  7237  genpassl  7325  genpassu  7326  elnnnn0  9013  peano2z  9083  znnsub  9098  znn0sub  9112  uzin  9351  nn01to3  9402  rpnegap  9467  negelrp  9468  xsubge0  9657  divelunit  9778  elfz5  9791  uzsplit  9865  elfzonelfzo  10000  adddivflid  10058  divfl0  10062  2shfti  10596  rexuz3  10755  clim2c  11046  fisumss  11154  infssuzex  11631  bezoutlemmain  11675  eltg3  12215  lmbrf  12373  cnrest2  12394  cnptoprest  12397  cnptoprest2  12398  ismet2  12512  elbl2ps  12550  elbl2  12551  xblpnfps  12556  xblpnf  12557  bdxmet  12659  metcn  12672  cnbl0  12692  cnblcld  12693  mulc1cncf  12734  ellimc3apf  12787  pilem1  12849