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  1510  elrab3t  3647  reuxfr1d  3711  n0moeu  4310  eldifvsn  4762  xpco  6318  funcnv3  6640  fnssresb  6691  dff1o5  6864  fneqeql2  7077  dffo3  7134  dffo3f  7138  fmptco  7162  fconst4  7251  riota2df  7431  eloprabga  7560  fnwelem  8180  frxp2  8198  xpord2pred  8199  xpord3pred  8206  mptsuppd  8242  mptelixpg  9001  boxcutc  9007  inficl  9454  cantnfle  9709  cantnflem1  9727  ttrclselem2  9764  bnd2  9993  iscard2  10094  alephinit  10213  kmlem2  10269  cfss  10382  fpwwe2lem8  10762  axgroth2  10949  elnnnn0  12689  znnsub  12782  znn0sub  12783  negelrp  13195  xsubge0  13431  divelunit  13665  elfz5  13688  preduz  13824  injresinj  13966  adddivflid  13998  divfl0  14004  hashf1lem1  14641  swrdspsleq  14857  repswsymball  14972  repswsymballbi  14973  2shfti  15276  cnpart  15450  sqrtneglem  15476  rexuz3  15560  rlim  15706  rlim2  15707  clim2c  15716  cvgcmp  16027  bitsmod  16650  bitscmp  16652  pc2dvds  17101  prmreclem4  17141  1arith  17149  imasleval  17763  xpsfrnel  17784  xpsfrnel2  17786  dfiso2  17997  pospropd  18549  latleeqm1  18691  latnlemlt  18696  latnle  18697  ipole  18758  gsumval2a  18924  ismhm0  19035  ghmeqker  19507  gastacos  19575  isslw  19873  slwpss  19877  pgpssslw  19879  fislw  19890  sylow3lem6  19897  dprd2d2  20311  isrnghmmul  20723  isdomn3  21017  isdrng4  21043  lsslss  21287  lsmspsn  21410  zndvds  21910  znleval2  21916  elfilspd  22164  islinds2  22174  islindf2  22175  ismhp3  22518  coe1mul2lem1  22641  matunitlindf  23051  eltg3  23335  leordtvallem1  23583  leordtvallem2  23584  lmbrf  23633  cnrest2  23659  xkoccn  23993  hauseqlcld  24020  qtopcn  24088  ordthmeolem  24175  isfbas  24203  fbunfip  24243  fixufil  24296  alexsubALTlem4  24424  ismet2  24707  xblpnfps  24769  xblpnf  24770  blval2  24936  metuel2  24939  dscopn  24947  cnbl0  25147  cnblcld  25148  xrtgioo  25181  mulc1cncf  25281  isclmp  25473  isncvsngp  25525  lmmbrf  25638  iscauf  25656  caucfil  25659  lmclim  25679  evthicc2  25836  volsup  25932  ioombl1lem4  25937  ismbf  26004  ismbfcn  26005  mbfmulc2lem  26023  mbfmax  26025  mbfposr  26028  ismbf3d  26030  mbfimaopnlem  26031  mbfsup  26040  i1fpos  26082  mbfi1fseqlem4  26094  xrge0f  26107  itg2seq  26118  itg2monolem1  26126  itg2gt0  26136  itg2cnlem1  26137  itg2cnlem2  26138  i1fibl  26183  ditgneg  26232  lhop1  26389  r1pid2  26535  fta1  26684  ulm2  26769  pilem1  26835  sineq0  26909  ellogrn  26944  rlimcnp  27350  wilthlem1  27452  sqff1o  27566  logfaclbnd  27606  bposlem1  27668  lgsdilem  27708  lgsabs1  27720  lgsdchrval  27738  lgsquadlem1  27764  lgsquadlem2  27765  sltssnb  28212  zn0subs  28846  iscgrgd  29033  trgcgrg  29035  ltgov  29117  ishlg  29125  lnhl  29138  israg  29229  islnopp  29272  elplng  29315  plngcplem  29320  iscgra  29373  isinag  29414  iseqlg  29469  dfprlng2  29482  nbupgrel  29983  isuvtx  30033  iscplgredg  30055  rusgrnumwwlkl1  30617  clwlkclwwlk2  30651  isclwwlknx  30684  clwwlkn1  30689  nmoo0  31450  ubthlem1  31529  ch0pss  32104  pjnorm2  32386  adjval  32549  leop  32782  atcv0eq  33038  xppreima  33337  fmptcof2  33349  xrdifh  33468  hashgt1  33496  isinftm  33841  isunit3  33900  rlocisunit  33936  fracerl  33972  dvdsruassoi  34043  dvdsruasso  34044  dvdsrspss  34046  lsmsnorb  34050  ply1degltel  34229  psrbasfsupp  34254  smatrcl  34539  rhmpreimacnlem  34627  ismntop  34769  brfae  34992  eulerpartlemr  35117  eulerpartlemn  35124  reprinrn  35358  reprinfz1  35362  reprdifc  35367  bnj1173  35743  dfscott3  35868  subfacp1lem5  36157  rexxfr3dALT  36612  filnetlem4  37384  mh-infprim1bi  37549  bj-clel3gALT  38233  bj-imdirco  38379  taupilem3  38508  topdifinffinlem  38538  finxpsuclem  38588  poimirlem22  38828  poimirlem26  38832  poimirlem27  38833  heicant  38841  mbfposadd  38853  itg2addnclem  38857  itg2addnclem2  38858  iblabsnclem  38869  ftc1anclem1  38879  ftc1anclem5  38883  areacirclem5  38898  areacirc  38899  lmclim2  38958  caures  38960  rrnheibor  39037  isdmn3  39274  opelvvdif  39462  ralrnmo  39559  raldmqsmo  39561  brxrn  39581  lrelat  40337  lcvbr  40344  lsatcv0eq  40370  ellkr2  40414  lkr0f  40417  lkreqN  40493  opltn0  40513  op1le  40515  leatb  40615  atlltn0  40629  hlrelat5N  40724  hlrelat  40725  cvrval5  40738  cvrexchlem  40742  atcvr0eq  40749  athgt  40779  1cvrco  40795  islpln5  40858  islvol5  40902  elpadd2at2  41130  cdleme0ex2N  41547  cdleme3  41560  cdleme7  41572  cdlemg33e  42033  dochfln0  42800  lcfl1  42815  lcfls1N  42858  lspindp5  43093  isnacs2  43983  rabrenfdioph  44087  rmxycomplete  44190  expdioph  44296  pwfi2f1o  44364  islnr3  44382  sqrtcvallem1  44892  ntrneixb  45356  clim2cf  46933  tmachlem-agreeprod  48220  funressnfv  48386  focofob  48423  nprmmul1  48882  oddm1evenALTV  49046  oddp1evenALTV  49047  divgcdoddALTV  49053  isidom3  49773  lco0  49870  lindslinindsimp2lem5  49905  snlindsntor  49914  elbigo2  49995  affinecomb1  50145  itscnhlinecirc02p  50228  reuxfr1dd  50248  iscnrm3lem1  50379