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  1778  elrab3t  2867  bnd2  4135  opbrop  4666  opelresi  4878  funcnv3  5233  fnssresb  5283  dff1o5  5424  fneqeql2  5577  fnniniseg2  5591  rexsupp  5592  dffo3  5615  fmptco  5634  fnressn  5654  fconst4m  5688  riota2df  5801  eloprabga  5909  frecabcl  6347  mptelixpg  6680  exmidfodomrlemreseldju  7136  enq0breq  7357  genpassl  7445  genpassu  7446  elnnnn0  9134  peano2z  9204  znnsub  9219  znn0sub  9233  uzin  9472  nn01to3  9527  rpnegap  9594  negelrp  9595  xsubge0  9786  divelunit  9907  elfz5  9921  uzsplit  9995  elfzonelfzo  10133  adddivflid  10195  divfl0  10199  2shfti  10735  rexuz3  10894  clim2c  11185  fisumss  11293  infssuzex  11840  bezoutlemmain  11886  eltg3  12499  lmbrf  12657  cnrest2  12678  cnptoprest  12681  cnptoprest2  12682  ismet2  12796  elbl2ps  12834  elbl2  12835  xblpnfps  12840  xblpnf  12841  bdxmet  12943  metcn  12956  cnbl0  12976  cnblcld  12977  mulc1cncf  13018  ellimc3apf  13071  pilem1  13142