MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantrurd Structured version   Visualization version   GIF version

Theorem biantrurd 524
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
StepHypRef Expression
1 biantrud.1 . 2 (𝜑𝜓)
2 ibar 520 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  mpbirand  690  3biant1d  1595  elrab3t  3557  n0moeu  4135  eldifvsn  4515  reuxfrd  5087  xpco  5886  funcnv3  6167  fnssresb  6211  dff1o5  6359  fneqeql2  6545  dffo3  6593  fmptco  6616  fconst4  6700  riota2df  6852  eloprabga  6974  fnwelem  7523  mptsuppd  7549  mptelixpg  8179  boxcutc  8185  inficl  8567  wemapso2lem  8693  cantnfle  8812  cantnflem1  8830  bnd2  9000  iscard2  9082  alephinit  9198  kmlem2  9255  cfss  9369  fpwwe2lem9  9742  axgroth2  9929  elnnnn0  11598  znnsub  11685  znn0sub  11686  uzin  11934  negelrp  12074  xsubge0  12305  supxrre1  12374  ixxun  12405  divelunit  12533  elfz5  12553  uzsplit  12631  preduz  12681  injresinj  12809  adddivflid  12839  divfl0  12845  hashf1lem1  13452  swrdspsleq  13669  repswsymball  13746  repswsymballbi  13747  2shfti  14039  cnpart  14199  sqrtneglem  14226  rexuz3  14307  rlim  14445  rlim2  14446  clim2c  14455  ello12  14466  elo12  14477  fsumss  14675  cvgcmp  14766  fprodss  14895  bitsmod  15373  bitscmp  15375  pc2dvds  15796  prmreclem4  15836  1arith  15844  ramval  15925  imasleval  16402  xpsfrnel  16424  xpsfrnel2  16426  dfiso2  16632  latleeqm1  17280  latnlemlt  17285  latnle  17286  pospropd  17335  ipole  17359  gsumval2a  17480  ghmeqker  17885  gastacos  17940  isslw  18220  slwpss  18224  pgpssslw  18226  fislw  18237  sylow3lem6  18244  dprd2d2  18641  lsslss  19164  lspsnel5  19198  lsmspsn  19287  coe1mul2lem1  19841  zndvds  20101  znleval2  20107  elfilspd  20348  islinds2  20358  islindf2  20359  eltg3  20976  leordtvallem1  21224  leordtvallem2  21225  lmbrf  21274  cnrest2  21300  cnprest  21303  cnprest2  21304  cnt0  21360  1stccn  21476  kgencn  21569  xkoccn  21632  qtopcn  21727  ordthmeolem  21814  isfbas  21842  fbunfip  21882  fixufil  21935  fbflim  21989  isflf  22006  cnflf  22015  fclscf  22038  cnfcf  22055  alexsubALTlem4  22063  ismet2  22347  elbl2ps  22403  elbl2  22404  xblpnfps  22409  xblpnf  22410  metcn  22557  txmetcn  22562  blval2  22576  metuel2  22579  dscopn  22587  cnbl0  22786  cnblcld  22787  xrtgioo  22818  mulc1cncf  22917  isclmp  23105  isncvsngp  23157  lmmbrf  23268  iscauf  23286  caucfil  23289  lmclim  23309  lmclimf  23310  evthicc2  23437  ovolfioo  23444  ovolficc  23445  ovoliun  23482  ismbl2  23504  volsup  23533  ioombl1lem4  23538  ismbf  23605  ismbfcn  23606  mbfmulc2lem  23624  mbfmax  23626  mbfposr  23629  ismbf3d  23631  mbfimaopnlem  23632  mbfaddlem  23637  mbfsup  23641  i1fpos  23683  mbfi1fseqlem4  23695  xrge0f  23708  itg2seq  23719  itg2monolem1  23727  itg2gt0  23737  itg2cnlem1  23738  itg2cnlem2  23739  i1fibl  23784  ditgneg  23831  lhop1  23987  fta1  24273  ulm2  24349  pilem1  24415  sineq0  24484  ellogrn  24516  rlimcnp  24902  wilthlem1  25004  sqff1o  25118  logfaclbnd  25157  bposlem1  25219  lgsdilem  25259  lgsabs1  25271  lgsdchrval  25289  lgsquadlem1  25315  lgsquadlem2  25316  iscgrgd  25618  trgcgrg  25620  tgellng  25658  ltgov  25702  ishlg  25707  lnhl  25720  israg  25802  islnopp  25841  iscgra  25911  isinag  25939  isleag  25943  iseqlg  25957  ttgelitv  25973  nbupgrel  26453  isuvtx  26511  isuvtxaOLD  26512  iscplgredg  26537  rusgrnumwwlkl1  27106  clwlkclwwlk2  27142  isclwwlknx  27180  clwwlkn1  27186  nmoo0  27971  ubthlem1  28051  ch0pss  28629  pjnorm2  28911  adjval  29074  leop  29307  atcv0eq  29563  reuxfr4d  29653  xppreima  29773  fmptcof2  29781  xrdifh  29866  isinftm  30057  smatrcl  30184  ismntoplly  30391  ismntop  30392  brfae  30633  eulerpartlemr  30758  eulerpartlemn  30765  reprinrn  31018  reprinfz1  31022  reprdifc  31027  bnj1173  31390  subfacp1lem5  31486  etasslt  32238  filnetlem4  32694  taupilem3  33479  topdifinffinlem  33508  finxpsuclem  33547  matunitlindf  33717  poimirlem22  33741  poimirlem26  33745  poimirlem27  33746  heicant  33754  mbfposadd  33766  itg2addnclem  33770  itg2addnclem2  33771  iblabsnclem  33782  ftc1anclem1  33794  ftc1anclem5  33798  areacirclem5  33813  areacirc  33814  lmclim2  33862  caures  33864  rrnheibor  33944  isdmn3  34181  opelvvdif  34338  brxrn  34446  lrelat  34791  lcvbr  34798  lsatcv0eq  34824  ellkr2  34868  lkr0f  34871  lkreqN  34947  opltn0  34967  op1le  34969  leatb  35069  atlltn0  35083  hlrelat5N  35178  hlrelat  35179  cvrval5  35192  cvrexchlem  35196  atcvr0eq  35203  athgt  35233  1cvrco  35249  islpln5  35312  islvol5  35356  elpadd2at2  35584  cdleme0ex2N  36002  cdleme3  36015  cdleme7  36027  cdlemg33e  36488  dochfln0  37255  lcfl1  37270  lcfls1N  37313  lspindp5  37548  isnacs2  37768  rabrenfdioph  37877  rmxycomplete  37980  expdioph  38088  pwfi2f1o  38164  islnr3  38183  isdomn3  38280  ntrneixb  38890  dffo3f  39850  clim2cf  40359  pfxsuffeqwrdeq  41978  oddm1evenALTV  42158  oddp1evenALTV  42159  divgcdoddALTV  42165  ismhm0  42370  isrnghmmul  42458  lco0  42781  lindslinindsimp2lem5  42816  snlindsntor  42825  elbigo2  42911
  Copyright terms: Public domain W3C validator