Theorem biantrurd 532

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm5.3  572  mpbirand  707  3biant1d  1480  elrab3t  3647  reuxfr1d  3710  n0moeu  4310  eldifvsn  4748  xpco  6237  funcnv3  6552  fnssresb  6604  dff1o5  6773  fneqeql2  6981  dffo3  7036  dffo3f  7040  fmptco  7063  fconst4  7150  riota2df  7329  eloprabga  7458  fnwelem  8064  frxp2  8077  xpord2pred  8078  xpord3pred  8085  mptsuppd  8120  mptelixpg  8862  boxcutc  8868  inficl  9315  cantnfle  9567  cantnflem1  9585  ttrclselem2  9622  bnd2  9789  iscard2  9872  alephinit  9989  kmlem2  10046  cfss  10159  fpwwe2lem8  10532  axgroth2  10719  elnnnn0  12427  znnsub  12521  znn0sub  12522  negelrp  12928  xsubge0  13163  divelunit  13397  elfz5  13419  preduz  13553  injresinj  13691  adddivflid  13722  divfl0  13728  hashf1lem1  14362  swrdspsleq  14572  repswsymball  14685  repswsymballbi  14686  2shfti  14987  cnpart  15147  sqrtneglem  15173  rexuz3  15256  rlim  15402  rlim2  15403  clim2c  15412  cvgcmp  15723  bitsmod  16347  bitscmp  16349  pc2dvds  16791  prmreclem4  16831  1arith  16839  imasleval  17445  xpsfrnel  17466  xpsfrnel2  17468  dfiso2  17679  pospropd  18231  latleeqm1  18373  latnlemlt  18378  latnle  18379  ipole  18440  gsumval2a  18559  ismhm0  18664  ghmeqker  19122  gastacos  19189  isslw  19487  slwpss  19491  pgpssslw  19493  fislw  19504  sylow3lem6  19511  dprd2d2  19925  isrnghmmul  20327  isdomn3  20600  lsslss  20864  lsmspsn  20988  zndvds  21456  znleval2  21462  elfilspd  21710  islinds2  21720  islindf2  21721  ismhp3  22027  coe1mul2lem1  22151  eltg3  22847  leordtvallem1  23095  leordtvallem2  23096  lmbrf  23145  cnrest2  23171  xkoccn  23504  hauseqlcld  23531  qtopcn  23599  ordthmeolem  23686  isfbas  23714  fbunfip  23754  fixufil  23807  alexsubALTlem4  23935  ismet2  24219  xblpnfps  24281  xblpnf  24282  blval2  24448  metuel2  24451  dscopn  24459  cnbl0  24659  cnblcld  24660  xrtgioo  24693  mulc1cncf  24796  isclmp  24995  isncvsngp  25047  lmmbrf  25160  iscauf  25178  caucfil  25181  lmclim  25201  evthicc2  25359  volsup  25455  ioombl1lem4  25460  ismbf  25527  ismbfcn  25528  mbfmulc2lem  25546  mbfmax  25548  mbfposr  25551  ismbf3d  25553  mbfimaopnlem  25554  mbfsup  25563  i1fpos  25605  mbfi1fseqlem4  25617  xrge0f  25630  itg2seq  25641  itg2monolem1  25649  itg2gt0  25659  itg2cnlem1  25660  itg2cnlem2  25661  i1fibl  25707  ditgneg  25756  lhop1  25917  r1pid2  26065  fta1  26214  ulm2  26292  pilem1  26359  sineq0  26431  ellogrn  26466  rlimcnp  26873  wilthlem1  26976  sqff1o  27090  logfaclbnd  27131  bposlem1  27193  lgsdilem  27233  lgsabs1  27245  lgsdchrval  27263  lgsquadlem1  27289  lgsquadlem2  27290  zn0subs  28296  iscgrgd  28458  trgcgrg  28460  ltgov  28542  ishlg  28547  lnhl  28560  israg  28642  islnopp  28684  iscgra  28754  isinag  28783  iseqlg  28812  nbupgrel  29290  isuvtx  29340  iscplgredg  29362  rusgrnumwwlkl1  29913  clwlkclwwlk2  29947  isclwwlknx  29980  clwwlkn1  29985  nmoo0  30735  ubthlem1  30814  ch0pss  31389  pjnorm2  31671  adjval  31834  leop  32067  atcv0eq  32323  xppreima  32588  fmptcof2  32600  xrdifh  32723  hashgt1  32753  isinftm  33123  isunit3  33181  isdrng4  33234  fracerl  33245  dvdsruassoi  33321  dvdsruasso  33322  dvdsrspss  33324  lsmsnorb  33328  ply1degltel  33527  r1pid2OLD  33541  psrbasfsupp  33544  smatrcl  33763  rhmpreimacnlem  33851  ismntop  33993  brfae  34215  eulerpartlemr  34342  eulerpartlemn  34349  reprinrn  34586  reprinfz1  34590  reprdifc  34595  bnj1173  34969  subfacp1lem5  35157  rexxfr3dALT  35612  filnetlem4  36355  bj-clel3gALT  37022  bj-imdirco  37164  taupilem3  37293  topdifinffinlem  37321  finxpsuclem  37371  matunitlindf  37598  poimirlem22  37622  poimirlem26  37626  poimirlem27  37627  heicant  37635  mbfposadd  37647  itg2addnclem  37651  itg2addnclem2  37652  iblabsnclem  37663  ftc1anclem1  37673  ftc1anclem5  37677  areacirclem5  37692  areacirc  37693  lmclim2  37738  caures  37740  rrnheibor  37817  isdmn3  38054  opelvvdif  38234  brxrn  38342  lrelat  38993  lcvbr  39000  lsatcv0eq  39026  ellkr2  39070  lkr0f  39073  lkreqN  39149  opltn0  39169  op1le  39171  leatb  39271  atlltn0  39285  hlrelat5N  39380  hlrelat  39381  cvrval5  39394  cvrexchlem  39398  atcvr0eq  39405  athgt  39435  1cvrco  39451  islpln5  39514  islvol5  39558  elpadd2at2  39786  cdleme0ex2N  40203  cdleme3  40216  cdleme7  40228  cdlemg33e  40689  dochfln0  41456  lcfl1  41471  lcfls1N  41514  lspindp5  41749  isnacs2  42679  rabrenfdioph  42787  rmxycomplete  42890  expdioph  42996  pwfi2f1o  43069  islnr3  43088  sqrtcvallem1  43604  ntrneixb  44068  clim2cf  45631  funressnfv  47027  focofob  47064  oddm1evenALTV  47659  oddp1evenALTV  47660  divgcdoddALTV  47666  lco0  48412  lindslinindsimp2lem5  48447  snlindsntor  48456  elbigo2  48537  affinecomb1  48687  itscnhlinecirc02p  48770  reuxfr1dd  48791  iscnrm3lem1  48918