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

Theorem biantrurd 528
 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 524 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383 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 197  df-an 385 This theorem is referenced by:  mpbirand  529  3biant1d  1481  elrab3t  3395  n0moeu  3970  eldifvsn  4359  reuxfrd  4923  xpco  5713  funcnv3  5997  fnssresb  6041  dff1o5  6184  fneqeql2  6366  dffo3  6414  fmptco  6436  fconst4  6519  riota2df  6671  eloprabga  6789  fnwelem  7337  mptsuppd  7363  mptelixpg  7987  boxcutc  7993  inficl  8372  wemapso2lem  8498  cantnfle  8606  cantnflem1  8624  bnd2  8794  iscard2  8840  alephinit  8956  kmlem2  9011  cfss  9125  fpwwe2lem9  9498  axgroth2  9685  elnnnn0  11374  znnsub  11461  znn0sub  11462  uzin  11758  negelrp  11902  xsubge0  12129  supxrre1  12198  ixxun  12229  divelunit  12352  elfz5  12372  uzsplit  12450  preduz  12500  injresinj  12629  adddivflid  12659  divfl0  12665  hashf1lem1  13277  swrdspsleq  13495  repswsymball  13572  repswsymballbi  13573  2shfti  13864  cnpart  14024  sqrtneglem  14051  rexuz3  14132  rlim  14270  rlim2  14271  clim2c  14280  ello12  14291  elo12  14302  fsumss  14500  fsumcom2OLD  14550  cvgcmp  14592  fprodss  14722  fprodcom2OLD  14759  bitsmod  15205  bitscmp  15207  pc2dvds  15630  prmreclem4  15670  1arith  15678  ramval  15759  imasleval  16248  xpsfrnel  16270  xpsfrnel2  16272  dfiso2  16479  latleeqm1  17126  latnlemlt  17131  latnle  17132  pospropd  17181  ipole  17205  gsumval2a  17326  ghmeqker  17734  gastacos  17789  isslw  18069  slwpss  18073  pgpssslw  18075  fislw  18086  sylow3lem6  18093  dprd2d2  18489  lsslss  19009  lspsnel5  19043  lsmspsn  19132  coe1mul2lem1  19685  zndvds  19946  znleval2  19952  elfilspd  20190  islinds2  20200  islindf2  20201  eltg3  20814  leordtvallem1  21062  leordtvallem2  21063  lmbrf  21112  cnrest2  21138  cnprest  21141  cnprest2  21142  cnt0  21198  1stccn  21314  kgencn  21407  xkoccn  21470  qtopcn  21565  ordthmeolem  21652  isfbas  21680  fbunfip  21720  fixufil  21773  fbflim  21827  isflf  21844  cnflf  21853  fclscf  21876  cnfcf  21893  alexsubALTlem4  21901  ismet2  22185  elbl2ps  22241  elbl2  22242  xblpnfps  22247  xblpnf  22248  metcn  22395  txmetcn  22400  blval2  22414  metuel2  22417  dscopn  22425  cnbl0  22624  cnblcld  22625  xrtgioo  22656  mulc1cncf  22755  isclmp  22943  isncvsngp  22995  lmmbrf  23106  iscauf  23124  caucfil  23127  lmclim  23147  lmclimf  23148  evthicc2  23275  ovolfioo  23282  ovolficc  23283  ovoliun  23319  ismbl2  23341  volsup  23370  ioombl1lem4  23375  ismbf  23442  ismbfcn  23443  mbfmulc2lem  23459  mbfmax  23461  mbfposr  23464  ismbf3d  23466  mbfimaopnlem  23467  mbfaddlem  23472  mbfsup  23476  i1fpos  23518  mbfi1fseqlem4  23530  xrge0f  23543  itg2seq  23554  itg2monolem1  23562  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  i1fibl  23619  ditgneg  23666  lhop1  23822  fta1  24108  ulm2  24184  pilem1  24250  sineq0  24318  ellogrn  24351  rlimcnp  24737  wilthlem1  24839  sqff1o  24953  logfaclbnd  24992  bposlem1  25054  lgsdilem  25094  lgsabs1  25106  lgsdchrval  25124  lgsquadlem1  25150  lgsquadlem2  25151  iscgrgd  25453  trgcgrg  25455  tgellng  25493  ltgov  25537  ishlg  25542  lnhl  25555  israg  25637  islnopp  25676  iscgra  25746  isinag  25774  isleag  25778  iseqlg  25792  ttgelitv  25808  nbupgrel  26286  isuvtx  26343  isuvtxaOLD  26344  iscplgredg  26369  rusgrnumwwlkl1  26935  clwlkclwwlk2  26969  isclwwlknx  26998  clwwlkn1  27004  nmoo0  27774  ubthlem1  27854  ch0pss  28432  pjnorm2  28714  adjval  28877  leop  29110  atcv0eq  29366  reuxfr4d  29457  xppreima  29577  fmptcof2  29585  xrdifh  29670  isinftm  29863  smatrcl  29990  ismntoplly  30197  ismntop  30198  brfae  30439  eulerpartlemr  30564  eulerpartlemn  30571  reprinrn  30824  reprinfz1  30828  reprdifc  30833  bnj1173  31196  subfacp1lem5  31292  etasslt  32045  filnetlem4  32501  taupilem3  33295  topdifinffinlem  33325  finxpsuclem  33364  matunitlindf  33537  poimirlem22  33561  poimirlem26  33565  poimirlem27  33566  heicant  33574  mbfposadd  33587  itg2addnclem  33591  itg2addnclem2  33592  iblabsnclem  33603  ftc1anclem1  33615  ftc1anclem5  33619  areacirclem5  33634  areacirc  33635  lmclim2  33684  caures  33686  rrnheibor  33766  isdmn3  34003  opelvvdif  34164  brxrn  34276  lrelat  34619  lcvbr  34626  lsatcv0eq  34652  ellkr2  34696  lkr0f  34699  lkreqN  34775  opltn0  34795  op1le  34797  leatb  34897  atlltn0  34911  hlrelat5N  35005  hlrelat  35006  cvrval5  35019  cvrexchlem  35023  atcvr0eq  35030  athgt  35060  1cvrco  35076  islpln5  35139  islvol5  35183  elpadd2at2  35411  cdleme0ex2N  35829  cdleme3  35842  cdleme7  35854  cdlemg33e  36315  dochfln0  37083  lcfl1  37098  lcfls1N  37141  lspindp5  37376  isnacs2  37586  rabrenfdioph  37695  rmxycomplete  37799  expdioph  37907  pwfi2f1o  37983  islnr3  38002  isdomn3  38099  ntrneixb  38710  dffo3f  39678  clim2cf  40200  pfxsuffeqwrdeq  41731  oddm1evenALTV  41911  oddp1evenALTV  41912  divgcdoddALTV  41918  ismhm0  42130  isrnghmmul  42218  lco0  42541  lindslinindsimp2lem5  42576  snlindsntor  42585  elbigo2  42671
 Copyright terms: Public domain W3C validator