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  6287  funcnv3  6603  fnssresb  6654  dff1o5  6827  fneqeql2  7039  dffo3  7095  dffo3f  7099  fmptco  7123  fconst4  7213  riota2df  7393  eloprabga  7522  fnwelem  8129  frxp2  8142  xpord2pred  8143  xpord3pred  8150  mptsuppd  8185  mptelixpg  8942  boxcutc  8948  inficl  9395  cantnfle  9650  cantnflem1  9668  ttrclselem2  9705  bnd2  9895  iscard2  9981  alephinit  10098  kmlem2  10154  cfss  10267  fpwwe2lem8  10647  axgroth2  10834  elnnnn0  12571  znnsub  12664  znn0sub  12665  negelrp  13077  xsubge0  13313  divelunit  13547  elfz5  13570  preduz  13705  injresinj  13847  adddivflid  13879  divfl0  13885  hashf1lem1  14520  swrdspsleq  14735  repswsymball  14850  repswsymballbi  14851  2shfti  15153  cnpart  15327  sqrtneglem  15353  rexuz3  15436  rlim  15582  rlim2  15583  clim2c  15592  cvgcmp  15903  bitsmod  16526  bitscmp  16528  pc2dvds  16971  prmreclem4  17011  1arith  17019  imasleval  17627  xpsfrnel  17648  xpsfrnel2  17650  dfiso2  17861  pospropd  18413  latleeqm1  18555  latnlemlt  18560  latnle  18561  ipole  18622  gsumval2a  18787  ismhm0  18898  ghmeqker  19370  gastacos  19437  isslw  19735  slwpss  19739  pgpssslw  19741  fislw  19752  sylow3lem6  19759  dprd2d2  20173  isrnghmmul  20583  isdomn3  20876  isdrng4  20902  lsslss  21145  lsmspsn  21268  zndvds  21762  znleval2  21768  elfilspd  22016  islinds2  22026  islindf2  22027  ismhp3  22370  coe1mul2lem1  22493  matunitlindf  22903  eltg3  23187  leordtvallem1  23435  leordtvallem2  23436  lmbrf  23485  cnrest2  23511  xkoccn  23845  hauseqlcld  23872  qtopcn  23940  ordthmeolem  24027  isfbas  24055  fbunfip  24095  fixufil  24148  alexsubALTlem4  24276  ismet2  24559  xblpnfps  24621  xblpnf  24622  blval2  24788  metuel2  24791  dscopn  24799  cnbl0  24999  cnblcld  25000  xrtgioo  25033  mulc1cncf  25133  isclmp  25325  isncvsngp  25377  lmmbrf  25490  iscauf  25508  caucfil  25511  lmclim  25531  evthicc2  25688  volsup  25784  ioombl1lem4  25789  ismbf  25856  ismbfcn  25857  mbfmulc2lem  25875  mbfmax  25877  mbfposr  25880  ismbf3d  25882  mbfimaopnlem  25883  mbfsup  25892  i1fpos  25934  mbfi1fseqlem4  25946  xrge0f  25959  itg2seq  25970  itg2monolem1  25978  itg2gt0  25988  itg2cnlem1  25989  itg2cnlem2  25990  i1fibl  26035  ditgneg  26084  lhop1  26241  r1pid2  26387  fta1  26538  ulm2  26621  pilem1  26687  sineq0  26761  ellogrn  26796  rlimcnp  27202  wilthlem1  27304  sqff1o  27418  logfaclbnd  27458  bposlem1  27520  lgsdilem  27560  lgsabs1  27572  lgsdchrval  27590  lgsquadlem1  27616  lgsquadlem2  27617  sltssnb  28034  zn0subs  28668  iscgrgd  28855  trgcgrg  28857  ltgov  28939  ishlg  28947  lnhl  28960  israg  29051  islnopp  29094  elplng  29137  plngcplem  29142  iscgra  29195  isinag  29236  iseqlg  29291  dfprlng2  29304  nbupgrel  29805  isuvtx  29855  iscplgredg  29877  rusgrnumwwlkl1  30439  clwlkclwwlk2  30473  isclwwlknx  30506  clwwlkn1  30511  nmoo0  31272  ubthlem1  31351  ch0pss  31926  pjnorm2  32208  adjval  32371  leop  32604  atcv0eq  32860  xppreima  33118  fmptcof2  33130  xrdifh  33251  hashgt1  33279  isinftm  33621  isunit3  33680  rlocisunit  33716  fracerl  33747  dvdsruassoi  33817  dvdsruasso  33818  dvdsrspss  33820  lsmsnorb  33824  ply1degltel  34004  psrbasfsupp  34021  smatrcl  34306  rhmpreimacnlem  34394  ismntop  34536  brfae  34759  eulerpartlemr  34885  eulerpartlemn  34892  reprinrn  35126  reprinfz1  35130  reprdifc  35135  bnj1173  35511  dfscott3  35626  subfacp1lem5  35763  rexxfr3dALT  36218  filnetlem4  37000  mh-infprim1bi  37165  bj-clel3gALT  37792  bj-imdirco  37942  taupilem3  38071  topdifinffinlem  38101  finxpsuclem  38151  poimirlem22  38391  poimirlem26  38395  poimirlem27  38396  heicant  38404  mbfposadd  38416  itg2addnclem  38420  itg2addnclem2  38421  iblabsnclem  38432  ftc1anclem1  38442  ftc1anclem5  38446  areacirclem5  38461  areacirc  38462  lmclim2  38508  caures  38510  rrnheibor  38587  isdmn3  38824  opelvvdif  39012  ralrnmo  39109  raldmqsmo  39111  brxrn  39131  lrelat  39887  lcvbr  39894  lsatcv0eq  39920  ellkr2  39964  lkr0f  39967  lkreqN  40043  opltn0  40063  op1le  40065  leatb  40165  atlltn0  40179  hlrelat5N  40274  hlrelat  40275  cvrval5  40288  cvrexchlem  40292  atcvr0eq  40299  athgt  40329  1cvrco  40345  islpln5  40408  islvol5  40452  elpadd2at2  40680  cdleme0ex2N  41097  cdleme3  41110  cdleme7  41122  cdlemg33e  41583  dochfln0  42350  lcfl1  42365  lcfls1N  42408  lspindp5  42643  isnacs2  43551  rabrenfdioph  43655  rmxycomplete  43758  expdioph  43864  pwfi2f1o  43937  islnr3  43956  sqrtcvallem1  44471  ntrneixb  44935  clim2cf  46478  tmachlem-agreeprod  47765  funressnfv  47931  focofob  47968  nprmmul1  48427  oddm1evenALTV  48591  oddp1evenALTV  48592  divgcdoddALTV  48598  isidom3  49260  lco0  49357  lindslinindsimp2lem5  49392  snlindsntor  49401  elbigo2  49482  affinecomb1  49632  itscnhlinecirc02p  49715  reuxfr1dd  49735  iscnrm3lem1  49860