Theorem biantrurd 541

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 537	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  pm5.3  582  mpbirand  719  3biant1d  1509  elrab3t  3649  reuxfr1d  3713  n0moeu  4314  eldifvsn  4765  xpco  6290  funcnv3  6606  fnssresb  6657  dff1o5  6830  fneqeql2  7042  dffo3  7097  dffo3f  7101  fmptco  7125  fconst4  7212  riota2df  7390  eloprabga  7519  fnwelem  8123  frxp2  8136  xpord2pred  8137  xpord3pred  8144  mptsuppd  8179  mptelixpg  8929  boxcutc  8935  inficl  9381  cantnfle  9636  cantnflem1  9654  ttrclselem2  9691  bnd2  9875  iscard2  9958  alephinit  10075  kmlem2  10131  cfss  10244  fpwwe2lem8  10618  axgroth2  10805  elnnnn0  12542  znnsub  12635  znn0sub  12636  negelrp  13046  xsubge0  13282  divelunit  13516  elfz5  13539  preduz  13674  injresinj  13816  adddivflid  13847  divfl0  13853  hashf1lem1  14488  swrdspsleq  14699  repswsymball  14812  repswsymballbi  14813  2shfti  15113  cnpart  15287  sqrtneglem  15313  rexuz3  15396  rlim  15542  rlim2  15543  clim2c  15552  cvgcmp  15864  bitsmod  16489  bitscmp  16491  pc2dvds  16934  prmreclem4  16974  1arith  16982  imasleval  17590  xpsfrnel  17611  xpsfrnel2  17613  dfiso2  17824  pospropd  18376  latleeqm1  18518  latnlemlt  18523  latnle  18524  ipole  18585  gsumval2a  18738  ismhm0  18843  ghmeqker  19308  gastacos  19375  isslw  19673  slwpss  19677  pgpssslw  19679  fislw  19690  sylow3lem6  19697  dprd2d2  20111  isrnghmmul  20520  isdomn3  20813  isdrng4  20839  lsslss  21082  lsmspsn  21205  zndvds  21699  znleval2  21705  elfilspd  21953  islinds2  21963  islindf2  21964  ismhp3  22305  coe1mul2lem1  22428  eltg3  23119  leordtvallem1  23367  leordtvallem2  23368  lmbrf  23417  cnrest2  23443  xkoccn  23776  hauseqlcld  23803  qtopcn  23871  ordthmeolem  23958  isfbas  23986  fbunfip  24026  fixufil  24079  alexsubALTlem4  24207  ismet2  24490  xblpnfps  24552  xblpnf  24553  blval2  24719  metuel2  24722  dscopn  24730  cnbl0  24930  cnblcld  24931  xrtgioo  24964  mulc1cncf  25064  isclmp  25256  isncvsngp  25308  lmmbrf  25421  iscauf  25439  caucfil  25442  lmclim  25462  evthicc2  25619  volsup  25715  ioombl1lem4  25720  ismbf  25787  ismbfcn  25788  mbfmulc2lem  25806  mbfmax  25808  mbfposr  25811  ismbf3d  25813  mbfimaopnlem  25814  mbfsup  25823  i1fpos  25865  mbfi1fseqlem4  25877  xrge0f  25890  itg2seq  25901  itg2monolem1  25909  itg2gt0  25919  itg2cnlem1  25920  itg2cnlem2  25921  i1fibl  25967  ditgneg  26016  lhop1  26173  r1pid2  26319  fta1  26469  ulm2  26548  pilem1  26614  sineq0  26689  ellogrn  26724  rlimcnp  27130  wilthlem1  27232  sqff1o  27346  logfaclbnd  27386  bposlem1  27448  lgsdilem  27488  lgsabs1  27500  lgsdchrval  27518  lgsquadlem1  27544  lgsquadlem2  27545  sltssnb  27962  zn0subs  28596  iscgrgd  28782  trgcgrg  28784  ltgov  28866  ishlg  28874  lnhl  28887  israg  28977  islnopp  29020  elplng  29062  plngcplem  29067  iscgra  29120  isinag  29155  iseqlg  29184  dfprlng2  29197  nbupgrel  29695  isuvtx  29745  iscplgredg  29767  rusgrnumwwlkl1  30320  clwlkclwwlk2  30354  isclwwlknx  30387  clwwlkn1  30392  nmoo0  31143  ubthlem1  31222  ch0pss  31797  pjnorm2  32079  adjval  32242  leop  32475  atcv0eq  32731  xppreima  32990  fmptcof2  33002  xrdifh  33125  hashgt1  33153  isinftm  33501  isunit3  33560  rlocisunit  33596  fracerl  33627  dvdsruassoi  33697  dvdsruasso  33698  dvdsrspss  33700  lsmsnorb  33704  ply1degltel  33884  psrbasfsupp  33901  smatrcl  34186  rhmpreimacnlem  34274  ismntop  34416  brfae  34638  eulerpartlemr  34764  eulerpartlemn  34771  reprinrn  35005  reprinfz1  35009  reprdifc  35014  bnj1173  35390  dfscott3  35512  subfacp1lem5  35676  rexxfr3dALT  36131  filnetlem4  36892  mh-infprim1bi  37057  bj-clel3gALT  37684  bj-imdirco  37834  taupilem3  37963  topdifinffinlem  37993  finxpsuclem  38043  matunitlindf  38269  poimirlem22  38293  poimirlem26  38297  poimirlem27  38298  heicant  38306  mbfposadd  38318  itg2addnclem  38322  itg2addnclem2  38323  iblabsnclem  38334  ftc1anclem1  38344  ftc1anclem5  38348  areacirclem5  38363  areacirc  38364  lmclim2  38409  caures  38411  rrnheibor  38488  isdmn3  38725  opelvvdif  38913  ralrnmo  39010  raldmqsmo  39012  brxrn  39032  lrelat  39788  lcvbr  39795  lsatcv0eq  39821  ellkr2  39865  lkr0f  39868  lkreqN  39944  opltn0  39964  op1le  39966  leatb  40066  atlltn0  40080  hlrelat5N  40175  hlrelat  40176  cvrval5  40189  cvrexchlem  40193  atcvr0eq  40200  athgt  40230  1cvrco  40246  islpln5  40309  islvol5  40353  elpadd2at2  40581  cdleme0ex2N  40998  cdleme3  41011  cdleme7  41023  cdlemg33e  41484  dochfln0  42251  lcfl1  42266  lcfls1N  42309  lspindp5  42544  isnacs2  43437  rabrenfdioph  43541  rmxycomplete  43644  expdioph  43750  pwfi2f1o  43823  islnr3  43842  sqrtcvallem1  44357  ntrneixb  44821  clim2cf  46364  funressnfv  47780  focofob  47817  nprmmul1  48276  oddm1evenALTV  48440  oddp1evenALTV  48441  divgcdoddALTV  48447  isidom3  49110  lco0  49207  lindslinindsimp2lem5  49242  snlindsntor  49251  elbigo2  49332  affinecomb1  49482  itscnhlinecirc02p  49565  reuxfr1dd  49585  iscnrm3lem1  49712