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  1189  3biant1d  1389  drex1  1844  elrab3t  2958  bnd2  4256  opbrop  4797  opelresi  5015  funcnv3  5382  fnssresb  5434  dff1o5  5580  fneqeql2  5743  fnniniseg2  5757  rexsupp  5758  dffo3  5781  fmptco  5800  fnressn  5824  fconst4m  5858  riota2df  5975  eloprabga  6090  frecabcl  6543  mptelixpg  6879  exmidfodomrlemreseldju  7374  enq0breq  7619  genpassl  7707  genpassu  7708  elnnnn0  9408  peano2z  9478  znnsub  9494  znn0sub  9508  uzin  9751  nn01to3  9808  rpnegap  9878  negelrp  9879  xsubge0  10073  divelunit  10194  elfz5  10209  uzsplit  10284  elfzonelfzo  10431  infssuzex  10448  adddivflid  10507  divfl0  10511  swrdspsleq  11194  2shfti  11337  rexuz3  11496  clim2c  11790  fisumss  11898  bitsmod  12462  bitscmp  12464  bezoutlemmain  12514  nninfctlemfo  12556  dvdsfi  12756  pc2dvds  12848  1arith  12885  xpsfrnel  13372  xpsfrnel2  13374  ghmeqker  13803  lsslss  14339  zndvds  14607  znleval2  14612  eltg3  14725  lmbrf  14883  cnrest2  14904  cnptoprest  14907  cnptoprest2  14908  ismet2  15022  elbl2ps  15060  elbl2  15061  xblpnfps  15066  xblpnf  15067  bdxmet  15169  metcn  15182  cnbl0  15202  cnblcld  15203  mulc1cncf  15257  ellimc3apf  15328  pilem1  15447  wilthlem1  15648  lgsdilem  15700  lgsne0  15711  lgsabs1  15712  lgsquadlem1  15750  lgsquadlem2  15751