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  1155  drex1  1786  elrab3t  2881  bnd2  4152  opbrop  4683  opelresi  4895  funcnv3  5250  fnssresb  5300  dff1o5  5441  fneqeql2  5594  fnniniseg2  5608  rexsupp  5609  dffo3  5632  fmptco  5651  fnressn  5671  fconst4m  5705  riota2df  5818  eloprabga  5929  frecabcl  6367  mptelixpg  6700  exmidfodomrlemreseldju  7156  enq0breq  7377  genpassl  7465  genpassu  7466  elnnnn0  9157  peano2z  9227  znnsub  9242  znn0sub  9256  uzin  9498  nn01to3  9555  rpnegap  9622  negelrp  9623  xsubge0  9817  divelunit  9938  elfz5  9952  uzsplit  10027  elfzonelfzo  10165  adddivflid  10227  divfl0  10231  2shfti  10773  rexuz3  10932  clim2c  11225  fisumss  11333  infssuzex  11882  bezoutlemmain  11931  pc2dvds  12261  1arith  12297  eltg3  12707  lmbrf  12865  cnrest2  12886  cnptoprest  12889  cnptoprest2  12890  ismet2  13004  elbl2ps  13042  elbl2  13043  xblpnfps  13048  xblpnf  13049  bdxmet  13151  metcn  13164  cnbl0  13184  cnblcld  13185  mulc1cncf  13226  ellimc3apf  13279  pilem1  13350  lgsdilem  13578  lgsne0  13589  lgsabs1  13590