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  1168  3biant1d  1367  drex1  1822  elrab3t  2932  bnd2  4225  opbrop  4762  opelresi  4979  funcnv3  5345  fnssresb  5397  dff1o5  5543  fneqeql2  5702  fnniniseg2  5716  rexsupp  5717  dffo3  5740  fmptco  5759  fnressn  5783  fconst4m  5817  riota2df  5933  eloprabga  6045  frecabcl  6498  mptelixpg  6834  exmidfodomrlemreseldju  7324  enq0breq  7569  genpassl  7657  genpassu  7658  elnnnn0  9358  peano2z  9428  znnsub  9444  znn0sub  9458  uzin  9701  nn01to3  9758  rpnegap  9828  negelrp  9829  xsubge0  10023  divelunit  10144  elfz5  10159  uzsplit  10234  elfzonelfzo  10381  infssuzex  10398  adddivflid  10457  divfl0  10461  swrdspsleq  11143  2shfti  11217  rexuz3  11376  clim2c  11670  fisumss  11778  bitsmod  12342  bitscmp  12344  bezoutlemmain  12394  nninfctlemfo  12436  dvdsfi  12636  pc2dvds  12728  1arith  12765  xpsfrnel  13251  xpsfrnel2  13253  ghmeqker  13682  lsslss  14218  zndvds  14486  znleval2  14491  eltg3  14604  lmbrf  14762  cnrest2  14783  cnptoprest  14786  cnptoprest2  14787  ismet2  14901  elbl2ps  14939  elbl2  14940  xblpnfps  14945  xblpnf  14946  bdxmet  15048  metcn  15061  cnbl0  15081  cnblcld  15082  mulc1cncf  15136  ellimc3apf  15207  pilem1  15326  wilthlem1  15527  lgsdilem  15579  lgsne0  15590  lgsabs1  15591  lgsquadlem1  15629  lgsquadlem2  15630