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  3643  reuxfr1d  3707  n0moeu  4306  eldifvsn  4756  xpco  6295  funcnv3  6615  fnssresb  6666  dff1o5  6839  fneqeql2  7051  dffo3  7107  dffo3f  7111  fmptco  7135  fconst4  7224  riota2df  7404  eloprabga  7533  fnwelem  8149  frxp2  8167  xpord2pred  8168  xpord3pred  8175  mptsuppd  8211  mptelixpg  8970  boxcutc  8976  inficl  9424  cantnfle  9679  cantnflem1  9697  ttrclselem2  9734  bnd2  9963  iscard2  10064  alephinit  10181  kmlem2  10237  cfss  10350  fpwwe2lem8  10730  axgroth2  10917  elnnnn0  12656  znnsub  12749  znn0sub  12750  negelrp  13162  xsubge0  13398  divelunit  13632  elfz5  13655  preduz  13791  injresinj  13933  adddivflid  13965  divfl0  13971  hashf1lem1  14607  swrdspsleq  14823  repswsymball  14938  repswsymballbi  14939  2shfti  15242  cnpart  15416  sqrtneglem  15442  rexuz3  15525  rlim  15671  rlim2  15672  clim2c  15681  cvgcmp  15992  bitsmod  16615  bitscmp  16617  pc2dvds  17066  prmreclem4  17106  1arith  17114  imasleval  17722  xpsfrnel  17743  xpsfrnel2  17745  dfiso2  17956  pospropd  18508  latleeqm1  18650  latnlemlt  18655  latnle  18656  ipole  18717  gsumval2a  18883  ismhm0  18994  ghmeqker  19466  gastacos  19533  isslw  19831  slwpss  19835  pgpssslw  19837  fislw  19848  sylow3lem6  19855  dprd2d2  20269  isrnghmmul  20681  isdomn3  20975  isdrng4  21001  lsslss  21245  lsmspsn  21368  zndvds  21864  znleval2  21870  elfilspd  22118  islinds2  22128  islindf2  22129  ismhp3  22472  coe1mul2lem1  22595  matunitlindf  23005  eltg3  23289  leordtvallem1  23537  leordtvallem2  23538  lmbrf  23587  cnrest2  23613  xkoccn  23947  hauseqlcld  23974  qtopcn  24042  ordthmeolem  24129  isfbas  24157  fbunfip  24197  fixufil  24250  alexsubALTlem4  24378  ismet2  24661  xblpnfps  24723  xblpnf  24724  blval2  24890  metuel2  24893  dscopn  24901  cnbl0  25101  cnblcld  25102  xrtgioo  25135  mulc1cncf  25235  isclmp  25427  isncvsngp  25479  lmmbrf  25592  iscauf  25610  caucfil  25613  lmclim  25633  evthicc2  25790  volsup  25886  ioombl1lem4  25891  ismbf  25958  ismbfcn  25959  mbfmulc2lem  25977  mbfmax  25979  mbfposr  25982  ismbf3d  25984  mbfimaopnlem  25985  mbfsup  25994  i1fpos  26036  mbfi1fseqlem4  26048  xrge0f  26061  itg2seq  26072  itg2monolem1  26080  itg2gt0  26090  itg2cnlem1  26091  itg2cnlem2  26092  i1fibl  26137  ditgneg  26186  lhop1  26343  r1pid2  26489  fta1  26638  ulm2  26721  pilem1  26787  sineq0  26861  ellogrn  26896  rlimcnp  27302  wilthlem1  27404  sqff1o  27518  logfaclbnd  27558  bposlem1  27620  lgsdilem  27660  lgsabs1  27672  lgsdchrval  27690  lgsquadlem1  27716  lgsquadlem2  27717  sltssnb  28164  zn0subs  28798  iscgrgd  28985  trgcgrg  28987  ltgov  29069  ishlg  29077  lnhl  29090  israg  29181  islnopp  29224  elplng  29267  plngcplem  29272  iscgra  29325  isinag  29366  iseqlg  29421  dfprlng2  29434  nbupgrel  29935  isuvtx  29985  iscplgredg  30007  rusgrnumwwlkl1  30569  clwlkclwwlk2  30603  isclwwlknx  30636  clwwlkn1  30641  nmoo0  31402  ubthlem1  31481  ch0pss  32056  pjnorm2  32338  adjval  32501  leop  32734  atcv0eq  32990  xppreima  33290  fmptcof2  33302  xrdifh  33422  hashgt1  33450  isinftm  33792  isunit3  33851  rlocisunit  33887  fracerl  33918  dvdsruassoi  33989  dvdsruasso  33990  dvdsrspss  33992  lsmsnorb  33996  ply1degltel  34176  psrbasfsupp  34193  smatrcl  34478  rhmpreimacnlem  34566  ismntop  34708  brfae  34931  eulerpartlemr  35056  eulerpartlemn  35063  reprinrn  35297  reprinfz1  35301  reprdifc  35306  bnj1173  35682  dfscott3  35801  subfacp1lem5  36039  rexxfr3dALT  36494  filnetlem4  37265  mh-infprim1bi  37430  bj-clel3gALT  38071  bj-imdirco  38220  taupilem3  38349  topdifinffinlem  38379  finxpsuclem  38429  poimirlem22  38669  poimirlem26  38673  poimirlem27  38674  heicant  38682  mbfposadd  38694  itg2addnclem  38698  itg2addnclem2  38699  iblabsnclem  38710  ftc1anclem1  38720  ftc1anclem5  38724  areacirclem5  38739  areacirc  38740  lmclim2  38801  caures  38803  rrnheibor  38880  isdmn3  39117  opelvvdif  39305  ralrnmo  39402  raldmqsmo  39404  brxrn  39424  lrelat  40180  lcvbr  40187  lsatcv0eq  40213  ellkr2  40257  lkr0f  40260  lkreqN  40336  opltn0  40356  op1le  40358  leatb  40458  atlltn0  40472  hlrelat5N  40567  hlrelat  40568  cvrval5  40581  cvrexchlem  40585  atcvr0eq  40592  athgt  40622  1cvrco  40638  islpln5  40701  islvol5  40745  elpadd2at2  40973  cdleme0ex2N  41390  cdleme3  41403  cdleme7  41415  cdlemg33e  41876  dochfln0  42643  lcfl1  42658  lcfls1N  42701  lspindp5  42936  isnacs2  43826  rabrenfdioph  43930  rmxycomplete  44033  expdioph  44139  pwfi2f1o  44207  islnr3  44226  sqrtcvallem1  44740  ntrneixb  45204  clim2cf  46768  tmachlem-agreeprod  48055  funressnfv  48221  focofob  48258  nprmmul1  48717  oddm1evenALTV  48881  oddp1evenALTV  48882  divgcdoddALTV  48888  isidom3  49550  lco0  49647  lindslinindsimp2lem5  49682  snlindsntor  49691  elbigo2  49772  affinecomb1  49922  itscnhlinecirc02p  50005  reuxfr1dd  50025  iscnrm3lem1  50156