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

Theorem biantrurd 533
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 529 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  pm5.3  573  mpbirand  703  3biant1d  1469  elrab3t  3678  reuxfr1d  3740  n0moeu  4315  eldifvsn  4724  xpco  6134  funcnv3  6418  fnssresb  6463  dff1o5  6618  fneqeql2  6810  dffo3  6861  fmptco  6884  fconst4  6969  riota2df  7126  eloprabga  7250  fnwelem  7816  mptsuppd  7844  mptelixpg  8488  boxcutc  8494  inficl  8878  cantnfle  9123  cantnflem1  9141  bnd2  9311  iscard2  9394  alephinit  9510  kmlem2  9566  cfss  9676  fpwwe2lem9  10049  axgroth2  10236  elnnnn0  11929  znnsub  12017  znn0sub  12018  negelrp  12412  xsubge0  12644  divelunit  12870  elfz5  12890  preduz  13019  injresinj  13148  adddivflid  13178  divfl0  13184  hashf1lem1  13803  swrdspsleq  14017  repswsymball  14131  repswsymballbi  14132  2shfti  14429  cnpart  14589  sqrtneglem  14616  rexuz3  14698  rlim  14842  rlim2  14843  clim2c  14852  cvgcmp  15161  bitsmod  15775  bitscmp  15777  pc2dvds  16205  prmreclem4  16245  1arith  16253  imasleval  16804  xpsfrnel  16825  xpsfrnel2  16827  dfiso2  17032  latleeqm1  17679  latnlemlt  17684  latnle  17685  pospropd  17734  ipole  17758  gsumval2a  17885  ghmeqker  18325  gastacos  18380  isslw  18664  slwpss  18668  pgpssslw  18670  fislw  18681  sylow3lem6  18688  dprd2d2  19097  lsslss  19664  lsmspsn  19787  mhpinvcl  20269  coe1mul2lem1  20365  zndvds  20626  znleval2  20632  elfilspd  20877  islinds2  20887  islindf2  20888  eltg3  21500  leordtvallem1  21748  leordtvallem2  21749  lmbrf  21798  cnrest2  21824  xkoccn  22157  hauseqlcld  22184  qtopcn  22252  ordthmeolem  22339  isfbas  22367  fbunfip  22407  fixufil  22460  alexsubALTlem4  22588  ismet2  22872  xblpnfps  22934  xblpnf  22935  blval2  23101  metuel2  23104  dscopn  23112  cnbl0  23311  cnblcld  23312  xrtgioo  23343  mulc1cncf  23442  isclmp  23630  isncvsngp  23682  lmmbrf  23794  iscauf  23812  caucfil  23815  lmclim  23835  evthicc2  23990  volsup  24086  ioombl1lem4  24091  ismbf  24158  ismbfcn  24159  mbfmulc2lem  24177  mbfmax  24179  mbfposr  24182  ismbf3d  24184  mbfimaopnlem  24185  mbfsup  24194  i1fpos  24236  mbfi1fseqlem4  24248  xrge0f  24261  itg2seq  24272  itg2monolem1  24280  itg2gt0  24290  itg2cnlem1  24291  itg2cnlem2  24292  i1fibl  24337  ditgneg  24384  lhop1  24540  fta1  24826  ulm2  24902  pilem1  24968  sineq0  25038  ellogrn  25070  rlimcnp  25471  wilthlem1  25573  sqff1o  25687  logfaclbnd  25726  bposlem1  25788  lgsdilem  25828  lgsabs1  25840  lgsdchrval  25858  lgsquadlem1  25884  lgsquadlem2  25885  iscgrgd  26227  trgcgrg  26229  ltgov  26311  ishlg  26316  lnhl  26329  israg  26411  islnopp  26453  iscgra  26523  isinag  26552  iseqlg  26581  nbupgrel  27055  isuvtx  27105  iscplgredg  27127  rusgrnumwwlkl1  27675  clwlkclwwlk2  27709  isclwwlknx  27742  clwwlkn1  27747  nmoo0  28496  ubthlem1  28575  ch0pss  29150  pjnorm2  29432  adjval  29595  leop  29828  atcv0eq  30084  xppreima  30323  fmptcof2  30331  xrdifh  30430  hashgt1  30457  isinftm  30738  smatrcl  30961  ismntop  31167  brfae  31407  eulerpartlemr  31532  eulerpartlemn  31539  reprinrn  31789  reprinfz1  31793  reprdifc  31798  bnj1173  32172  subfacp1lem5  32329  etasslt  33172  filnetlem4  33627  taupilem3  34483  topdifinffinlem  34511  finxpsuclem  34561  matunitlindf  34772  poimirlem22  34796  poimirlem26  34800  poimirlem27  34801  heicant  34809  mbfposadd  34821  itg2addnclem  34825  itg2addnclem2  34826  iblabsnclem  34837  ftc1anclem1  34849  ftc1anclem5  34853  areacirclem5  34868  areacirc  34869  lmclim2  34916  caures  34918  rrnheibor  34998  isdmn3  35235  opelvvdif  35403  brxrn  35508  lrelat  36032  lcvbr  36039  lsatcv0eq  36065  ellkr2  36109  lkr0f  36112  lkreqN  36188  opltn0  36208  op1le  36210  leatb  36310  atlltn0  36324  hlrelat5N  36419  hlrelat  36420  cvrval5  36433  cvrexchlem  36437  atcvr0eq  36444  athgt  36474  1cvrco  36490  islpln5  36553  islvol5  36597  elpadd2at2  36825  cdleme0ex2N  37242  cdleme3  37255  cdleme7  37267  cdlemg33e  37728  dochfln0  38495  lcfl1  38510  lcfls1N  38553  lspindp5  38788  isnacs2  39183  rabrenfdioph  39291  rmxycomplete  39394  expdioph  39500  pwfi2f1o  39576  islnr3  39595  isdomn3  39684  ntrneixb  40325  dffo3f  41318  clim2cf  41811  funressnfv  43159  oddm1evenALTV  43687  oddp1evenALTV  43688  divgcdoddALTV  43694  ismhm0  43919  isrnghmmul  44062  lco0  44380  lindslinindsimp2lem5  44415  snlindsntor  44424  elbigo2  44510  affinecomb1  44587  itscnhlinecirc02p  44670
  Copyright terms: Public domain W3C validator