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

Theorem biantrurd 535
 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 531 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  pm5.3  575  mpbirand  705  3biant1d  1471  elrab3t  3677  reuxfr1d  3739  n0moeu  4314  eldifvsn  4722  xpco  6133  funcnv3  6417  fnssresb  6462  dff1o5  6617  fneqeql2  6810  dffo3  6861  fmptco  6884  fconst4  6969  riota2df  7129  eloprabga  7253  fnwelem  7817  mptsuppd  7845  mptelixpg  8491  boxcutc  8497  inficl  8881  cantnfle  9126  cantnflem1  9144  bnd2  9314  iscard2  9397  alephinit  9513  kmlem2  9569  cfss  9679  fpwwe2lem9  10052  axgroth2  10239  elnnnn0  11932  znnsub  12020  znn0sub  12021  negelrp  12414  xsubge0  12646  divelunit  12872  elfz5  12892  preduz  13021  injresinj  13150  adddivflid  13180  divfl0  13186  hashf1lem1  13805  swrdspsleq  14019  repswsymball  14133  repswsymballbi  14134  2shfti  14431  cnpart  14591  sqrtneglem  14618  rexuz3  14700  rlim  14844  rlim2  14845  clim2c  14854  cvgcmp  15163  bitsmod  15777  bitscmp  15779  pc2dvds  16207  prmreclem4  16247  1arith  16255  imasleval  16806  xpsfrnel  16827  xpsfrnel2  16829  dfiso2  17034  latleeqm1  17681  latnlemlt  17686  latnle  17687  pospropd  17736  ipole  17760  gsumval2a  17887  ghmeqker  18377  gastacos  18432  isslw  18725  slwpss  18729  pgpssslw  18731  fislw  18742  sylow3lem6  18749  dprd2d2  19158  lsslss  19725  lsmspsn  19848  mhpinvcl  20331  coe1mul2lem1  20427  zndvds  20688  znleval2  20694  elfilspd  20939  islinds2  20949  islindf2  20950  eltg3  21562  leordtvallem1  21810  leordtvallem2  21811  lmbrf  21860  cnrest2  21886  xkoccn  22219  hauseqlcld  22246  qtopcn  22314  ordthmeolem  22401  isfbas  22429  fbunfip  22469  fixufil  22522  alexsubALTlem4  22650  ismet2  22935  xblpnfps  22997  xblpnf  22998  blval2  23164  metuel2  23167  dscopn  23175  cnbl0  23374  cnblcld  23375  xrtgioo  23406  mulc1cncf  23505  isclmp  23693  isncvsngp  23745  lmmbrf  23857  iscauf  23875  caucfil  23878  lmclim  23898  evthicc2  24053  volsup  24149  ioombl1lem4  24154  ismbf  24221  ismbfcn  24222  mbfmulc2lem  24240  mbfmax  24242  mbfposr  24245  ismbf3d  24247  mbfimaopnlem  24248  mbfsup  24257  i1fpos  24299  mbfi1fseqlem4  24311  xrge0f  24324  itg2seq  24335  itg2monolem1  24343  itg2gt0  24353  itg2cnlem1  24354  itg2cnlem2  24355  i1fibl  24400  ditgneg  24447  lhop1  24603  fta1  24889  ulm2  24965  pilem1  25031  sineq0  25101  ellogrn  25135  rlimcnp  25535  wilthlem1  25637  sqff1o  25751  logfaclbnd  25790  bposlem1  25852  lgsdilem  25892  lgsabs1  25904  lgsdchrval  25922  lgsquadlem1  25948  lgsquadlem2  25949  iscgrgd  26291  trgcgrg  26293  ltgov  26375  ishlg  26380  lnhl  26393  israg  26475  islnopp  26517  iscgra  26587  isinag  26616  iseqlg  26645  nbupgrel  27119  isuvtx  27169  iscplgredg  27191  rusgrnumwwlkl1  27739  clwlkclwwlk2  27773  isclwwlknx  27806  clwwlkn1  27811  nmoo0  28560  ubthlem1  28639  ch0pss  29214  pjnorm2  29496  adjval  29659  leop  29892  atcv0eq  30148  xppreima  30386  fmptcof2  30394  xrdifh  30495  hashgt1  30522  isinftm  30803  lsmsnorb  30938  smatrcl  31049  ismntop  31255  brfae  31495  eulerpartlemr  31620  eulerpartlemn  31627  reprinrn  31877  reprinfz1  31881  reprdifc  31886  bnj1173  32262  subfacp1lem5  32419  etasslt  33262  filnetlem4  33717  taupilem3  34587  topdifinffinlem  34615  finxpsuclem  34665  matunitlindf  34877  poimirlem22  34901  poimirlem26  34905  poimirlem27  34906  heicant  34914  mbfposadd  34926  itg2addnclem  34930  itg2addnclem2  34931  iblabsnclem  34942  ftc1anclem1  34954  ftc1anclem5  34958  areacirclem5  34973  areacirc  34974  lmclim2  35020  caures  35022  rrnheibor  35102  isdmn3  35339  opelvvdif  35507  brxrn  35613  lrelat  36137  lcvbr  36144  lsatcv0eq  36170  ellkr2  36214  lkr0f  36217  lkreqN  36293  opltn0  36313  op1le  36315  leatb  36415  atlltn0  36429  hlrelat5N  36524  hlrelat  36525  cvrval5  36538  cvrexchlem  36542  atcvr0eq  36549  athgt  36579  1cvrco  36595  islpln5  36658  islvol5  36702  elpadd2at2  36930  cdleme0ex2N  37347  cdleme3  37360  cdleme7  37372  cdlemg33e  37833  dochfln0  38600  lcfl1  38615  lcfls1N  38658  lspindp5  38893  isnacs2  39288  rabrenfdioph  39396  rmxycomplete  39499  expdioph  39605  pwfi2f1o  39681  islnr3  39700  isdomn3  39789  ntrneixb  40430  dffo3f  41422  clim2cf  41915  funressnfv  43263  oddm1evenALTV  43825  oddp1evenALTV  43826  divgcdoddALTV  43832  ismhm0  44057  isrnghmmul  44149  lco0  44467  lindslinindsimp2lem5  44502  snlindsntor  44511  elbigo2  44597  affinecomb1  44674  itscnhlinecirc02p  44757
 Copyright terms: Public domain W3C validator