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  3651  reuxfr1d  3715  n0moeu  4314  eldifvsn  4767  xpco  6294  funcnv3  6610  fnssresb  6661  dff1o5  6834  fneqeql2  7046  dffo3  7101  dffo3f  7105  fmptco  7129  fconst4  7219  riota2df  7399  eloprabga  7528  fnwelem  8133  frxp2  8146  xpord2pred  8147  xpord3pred  8154  mptsuppd  8189  mptelixpg  8939  boxcutc  8945  inficl  9392  cantnfle  9647  cantnflem1  9665  ttrclselem2  9702  bnd2  9892  iscard2  9978  alephinit  10095  kmlem2  10151  cfss  10264  fpwwe2lem8  10638  axgroth2  10825  elnnnn0  12562  znnsub  12655  znn0sub  12656  negelrp  13067  xsubge0  13303  divelunit  13537  elfz5  13560  preduz  13695  injresinj  13837  adddivflid  13869  divfl0  13875  hashf1lem1  14510  swrdspsleq  14725  repswsymball  14840  repswsymballbi  14841  2shfti  15141  cnpart  15315  sqrtneglem  15341  rexuz3  15424  rlim  15570  rlim2  15571  clim2c  15580  cvgcmp  15891  bitsmod  16516  bitscmp  16518  pc2dvds  16961  prmreclem4  17001  1arith  17009  imasleval  17617  xpsfrnel  17638  xpsfrnel2  17640  dfiso2  17851  pospropd  18403  latleeqm1  18545  latnlemlt  18550  latnle  18551  ipole  18612  gsumval2a  18775  ismhm0  18885  ghmeqker  19357  gastacos  19424  isslw  19722  slwpss  19726  pgpssslw  19728  fislw  19739  sylow3lem6  19746  dprd2d2  20160  isrnghmmul  20570  isdomn3  20863  isdrng4  20889  lsslss  21132  lsmspsn  21255  zndvds  21749  znleval2  21755  elfilspd  22003  islinds2  22013  islindf2  22014  ismhp3  22355  coe1mul2lem1  22478  eltg3  23169  leordtvallem1  23417  leordtvallem2  23418  lmbrf  23467  cnrest2  23493  xkoccn  23827  hauseqlcld  23854  qtopcn  23922  ordthmeolem  24009  isfbas  24037  fbunfip  24077  fixufil  24130  alexsubALTlem4  24258  ismet2  24541  xblpnfps  24603  xblpnf  24604  blval2  24770  metuel2  24773  dscopn  24781  cnbl0  24981  cnblcld  24982  xrtgioo  25015  mulc1cncf  25115  isclmp  25307  isncvsngp  25359  lmmbrf  25472  iscauf  25490  caucfil  25493  lmclim  25513  evthicc2  25670  volsup  25766  ioombl1lem4  25771  ismbf  25838  ismbfcn  25839  mbfmulc2lem  25857  mbfmax  25859  mbfposr  25862  ismbf3d  25864  mbfimaopnlem  25865  mbfsup  25874  i1fpos  25916  mbfi1fseqlem4  25928  xrge0f  25941  itg2seq  25952  itg2monolem1  25960  itg2gt0  25970  itg2cnlem1  25971  itg2cnlem2  25972  i1fibl  26018  ditgneg  26067  lhop1  26224  r1pid2  26370  fta1  26520  ulm2  26599  pilem1  26665  sineq0  26740  ellogrn  26775  rlimcnp  27181  wilthlem1  27283  sqff1o  27397  logfaclbnd  27437  bposlem1  27499  lgsdilem  27539  lgsabs1  27551  lgsdchrval  27569  lgsquadlem1  27595  lgsquadlem2  27596  sltssnb  28013  zn0subs  28647  iscgrgd  28833  trgcgrg  28835  ltgov  28917  ishlg  28925  lnhl  28938  israg  29028  islnopp  29071  elplng  29113  plngcplem  29118  iscgra  29171  isinag  29210  iseqlg  29239  dfprlng2  29252  nbupgrel  29753  isuvtx  29803  iscplgredg  29825  rusgrnumwwlkl1  30387  clwlkclwwlk2  30421  isclwwlknx  30454  clwwlkn1  30459  nmoo0  31214  ubthlem1  31293  ch0pss  31868  pjnorm2  32150  adjval  32313  leop  32546  atcv0eq  32802  xppreima  33061  fmptcof2  33073  xrdifh  33195  hashgt1  33223  isinftm  33565  isunit3  33624  rlocisunit  33660  fracerl  33691  dvdsruassoi  33761  dvdsruasso  33762  dvdsrspss  33764  lsmsnorb  33768  ply1degltel  33948  psrbasfsupp  33965  smatrcl  34250  rhmpreimacnlem  34338  ismntop  34480  brfae  34703  eulerpartlemr  34829  eulerpartlemn  34836  reprinrn  35070  reprinfz1  35074  reprdifc  35079  bnj1173  35455  dfscott3  35570  subfacp1lem5  35713  rexxfr3dALT  36168  filnetlem4  36949  mh-infprim1bi  37114  bj-clel3gALT  37741  bj-imdirco  37891  taupilem3  38020  topdifinffinlem  38050  finxpsuclem  38100  matunitlindf  38326  poimirlem22  38350  poimirlem26  38354  poimirlem27  38355  heicant  38363  mbfposadd  38375  itg2addnclem  38379  itg2addnclem2  38380  iblabsnclem  38391  ftc1anclem1  38401  ftc1anclem5  38405  areacirclem5  38420  areacirc  38421  lmclim2  38467  caures  38469  rrnheibor  38546  isdmn3  38783  opelvvdif  38971  ralrnmo  39068  raldmqsmo  39070  brxrn  39090  lrelat  39846  lcvbr  39853  lsatcv0eq  39879  ellkr2  39923  lkr0f  39926  lkreqN  40002  opltn0  40022  op1le  40024  leatb  40124  atlltn0  40138  hlrelat5N  40233  hlrelat  40234  cvrval5  40247  cvrexchlem  40251  atcvr0eq  40258  athgt  40288  1cvrco  40304  islpln5  40367  islvol5  40411  elpadd2at2  40639  cdleme0ex2N  41056  cdleme3  41069  cdleme7  41081  cdlemg33e  41542  dochfln0  42309  lcfl1  42324  lcfls1N  42367  lspindp5  42602  isnacs2  43495  rabrenfdioph  43599  rmxycomplete  43702  expdioph  43808  pwfi2f1o  43881  islnr3  43900  sqrtcvallem1  44415  ntrneixb  44879  clim2cf  46422  funressnfv  47838  focofob  47875  nprmmul1  48334  oddm1evenALTV  48498  oddp1evenALTV  48499  divgcdoddALTV  48505  isidom3  49167  lco0  49264  lindslinindsimp2lem5  49299  snlindsntor  49308  elbigo2  49389  affinecomb1  49539  itscnhlinecirc02p  49622  reuxfr1dd  49642  iscnrm3lem1  49769