Theorem biantrurd 542

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm5.3  583  mpbirand  720  3biant1d  1509  elrab3t  3644  reuxfr1d  3708  n0moeu  4307  eldifvsn  4760  xpco  6291  funcnv3  6608  fnssresb  6659  dff1o5  6832  fneqeql2  7044  dffo3  7100  dffo3f  7104  fmptco  7128  fconst4  7218  riota2df  7398  eloprabga  7527  fnwelem  8141  frxp2  8154  xpord2pred  8155  xpord3pred  8162  mptsuppd  8197  mptelixpg  8956  boxcutc  8962  inficl  9410  cantnfle  9665  cantnflem1  9683  ttrclselem2  9720  bnd2  9949  iscard2  10050  alephinit  10167  kmlem2  10223  cfss  10336  fpwwe2lem8  10716  axgroth2  10903  elnnnn0  12642  znnsub  12735  znn0sub  12736  negelrp  13148  xsubge0  13384  divelunit  13618  elfz5  13641  preduz  13777  injresinj  13919  adddivflid  13951  divfl0  13957  hashf1lem1  14593  swrdspsleq  14808  repswsymball  14923  repswsymballbi  14924  2shfti  15226  cnpart  15400  sqrtneglem  15426  rexuz3  15509  rlim  15655  rlim2  15656  clim2c  15665  cvgcmp  15976  bitsmod  16599  bitscmp  16601  pc2dvds  17050  prmreclem4  17090  1arith  17098  imasleval  17706  xpsfrnel  17727  xpsfrnel2  17729  dfiso2  17940  pospropd  18492  latleeqm1  18634  latnlemlt  18639  latnle  18640  ipole  18701  gsumval2a  18867  ismhm0  18978  ghmeqker  19450  gastacos  19517  isslw  19815  slwpss  19819  pgpssslw  19821  fislw  19832  sylow3lem6  19839  dprd2d2  20253  isrnghmmul  20665  isdomn3  20959  isdrng4  20985  lsslss  21229  lsmspsn  21352  zndvds  21848  znleval2  21854  elfilspd  22102  islinds2  22112  islindf2  22113  ismhp3  22456  coe1mul2lem1  22579  matunitlindf  22989  eltg3  23273  leordtvallem1  23521  leordtvallem2  23522  lmbrf  23571  cnrest2  23597  xkoccn  23931  hauseqlcld  23958  qtopcn  24026  ordthmeolem  24113  isfbas  24141  fbunfip  24181  fixufil  24234  alexsubALTlem4  24362  ismet2  24645  xblpnfps  24707  xblpnf  24708  blval2  24874  metuel2  24877  dscopn  24885  cnbl0  25085  cnblcld  25086  xrtgioo  25119  mulc1cncf  25219  isclmp  25411  isncvsngp  25463  lmmbrf  25576  iscauf  25594  caucfil  25597  lmclim  25617  evthicc2  25774  volsup  25870  ioombl1lem4  25875  ismbf  25942  ismbfcn  25943  mbfmulc2lem  25961  mbfmax  25963  mbfposr  25966  ismbf3d  25968  mbfimaopnlem  25969  mbfsup  25978  i1fpos  26020  mbfi1fseqlem4  26032  xrge0f  26045  itg2seq  26056  itg2monolem1  26064  itg2gt0  26074  itg2cnlem1  26075  itg2cnlem2  26076  i1fibl  26121  ditgneg  26170  lhop1  26327  r1pid2  26473  fta1  26622  ulm2  26705  pilem1  26771  sineq0  26845  ellogrn  26880  rlimcnp  27286  wilthlem1  27388  sqff1o  27502  logfaclbnd  27542  bposlem1  27604  lgsdilem  27644  lgsabs1  27656  lgsdchrval  27674  lgsquadlem1  27700  lgsquadlem2  27701  sltssnb  28148  zn0subs  28782  iscgrgd  28969  trgcgrg  28971  ltgov  29053  ishlg  29061  lnhl  29074  israg  29165  islnopp  29208  elplng  29251  plngcplem  29256  iscgra  29309  isinag  29350  iseqlg  29405  dfprlng2  29418  nbupgrel  29919  isuvtx  29969  iscplgredg  29991  rusgrnumwwlkl1  30553  clwlkclwwlk2  30587  isclwwlknx  30620  clwwlkn1  30625  nmoo0  31386  ubthlem1  31465  ch0pss  32040  pjnorm2  32322  adjval  32485  leop  32718  atcv0eq  32974  xppreima  33232  fmptcof2  33244  xrdifh  33365  hashgt1  33393  isinftm  33735  isunit3  33794  rlocisunit  33830  fracerl  33861  dvdsruassoi  33932  dvdsruasso  33933  dvdsrspss  33935  lsmsnorb  33939  ply1degltel  34119  psrbasfsupp  34136  smatrcl  34421  rhmpreimacnlem  34509  ismntop  34651  brfae  34874  eulerpartlemr  34999  eulerpartlemn  35006  reprinrn  35240  reprinfz1  35244  reprdifc  35249  bnj1173  35625  dfscott3  35731  subfacp1lem5  35928  rexxfr3dALT  36383  filnetlem4  37149  mh-infprim1bi  37314  bj-clel3gALT  37943  bj-imdirco  38091  taupilem3  38220  topdifinffinlem  38250  finxpsuclem  38300  poimirlem22  38540  poimirlem26  38544  poimirlem27  38545  heicant  38553  mbfposadd  38565  itg2addnclem  38569  itg2addnclem2  38570  iblabsnclem  38581  ftc1anclem1  38591  ftc1anclem5  38595  areacirclem5  38610  areacirc  38611  lmclim2  38672  caures  38674  rrnheibor  38751  isdmn3  38988  opelvvdif  39176  ralrnmo  39273  raldmqsmo  39275  brxrn  39295  lrelat  40051  lcvbr  40058  lsatcv0eq  40084  ellkr2  40128  lkr0f  40131  lkreqN  40207  opltn0  40227  op1le  40229  leatb  40329  atlltn0  40343  hlrelat5N  40438  hlrelat  40439  cvrval5  40452  cvrexchlem  40456  atcvr0eq  40463  athgt  40493  1cvrco  40509  islpln5  40572  islvol5  40616  elpadd2at2  40844  cdleme0ex2N  41261  cdleme3  41274  cdleme7  41286  cdlemg33e  41747  dochfln0  42514  lcfl1  42529  lcfls1N  42572  lspindp5  42807  isnacs2  43696  rabrenfdioph  43800  rmxycomplete  43903  expdioph  44009  pwfi2f1o  44082  islnr3  44101  sqrtcvallem1  44616  ntrneixb  45080  clim2cf  46629  tmachlem-agreeprod  47916  funressnfv  48082  focofob  48119  nprmmul1  48578  oddm1evenALTV  48742  oddp1evenALTV  48743  divgcdoddALTV  48749  isidom3  49411  lco0  49508  lindslinindsimp2lem5  49543  snlindsntor  49552  elbigo2  49633  affinecomb1  49783  itscnhlinecirc02p  49866  reuxfr1dd  49886  iscnrm3lem1  50011