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

Theorem biantrurd 536
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 532 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 17 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  pm5.3  576  mpbirand  707  3biant1d  1480  elrab3t  3613  reuxfr1d  3677  n0moeu  4285  eldifvsn  4724  xpco  6166  funcnv3  6467  fnssresb  6517  dff1o5  6688  fneqeql2  6885  dffo3  6939  fmptco  6962  fconst4  7048  riota2df  7212  eloprabga  7336  eloprabgaOLD  7337  fnwelem  7918  mptsuppd  7949  mptelixpg  8636  boxcutc  8642  inficl  9065  cantnfle  9310  cantnflem1  9328  bnd2  9533  iscard2  9616  alephinit  9733  kmlem2  9789  cfss  9903  fpwwe2lem8  10276  axgroth2  10463  elnnnn0  12157  znnsub  12247  znn0sub  12248  negelrp  12643  xsubge0  12875  divelunit  13106  elfz5  13128  preduz  13258  injresinj  13387  adddivflid  13417  divfl0  13423  hashf1lem1  14044  hashf1lem1OLD  14045  swrdspsleq  14254  repswsymball  14368  repswsymballbi  14369  2shfti  14667  cnpart  14827  sqrtneglem  14854  rexuz3  14936  rlim  15080  rlim2  15081  clim2c  15090  cvgcmp  15404  bitsmod  16019  bitscmp  16021  pc2dvds  16456  prmreclem4  16496  1arith  16504  imasleval  17070  xpsfrnel  17091  xpsfrnel2  17093  dfiso2  17301  pospropd  17857  latleeqm1  17997  latnlemlt  18002  latnle  18003  ipole  18064  gsumval2a  18181  ghmeqker  18673  gastacos  18728  isslw  19021  slwpss  19025  pgpssslw  19027  fislw  19038  sylow3lem6  19045  dprd2d2  19455  lsslss  20022  lsmspsn  20145  zndvds  20538  znleval2  20544  elfilspd  20789  islinds2  20799  islindf2  20800  ismhp3  21107  coe1mul2lem1  21212  eltg3  21883  leordtvallem1  22131  leordtvallem2  22132  lmbrf  22181  cnrest2  22207  xkoccn  22540  hauseqlcld  22567  qtopcn  22635  ordthmeolem  22722  isfbas  22750  fbunfip  22790  fixufil  22843  alexsubALTlem4  22971  ismet2  23255  xblpnfps  23317  xblpnf  23318  blval2  23484  metuel2  23487  dscopn  23495  cnbl0  23695  cnblcld  23696  xrtgioo  23727  mulc1cncf  23826  isclmp  24018  isncvsngp  24070  lmmbrf  24183  iscauf  24201  caucfil  24204  lmclim  24224  evthicc2  24381  volsup  24477  ioombl1lem4  24482  ismbf  24549  ismbfcn  24550  mbfmulc2lem  24568  mbfmax  24570  mbfposr  24573  ismbf3d  24575  mbfimaopnlem  24576  mbfsup  24585  i1fpos  24628  mbfi1fseqlem4  24640  xrge0f  24653  itg2seq  24664  itg2monolem1  24672  itg2gt0  24682  itg2cnlem1  24683  itg2cnlem2  24684  i1fibl  24729  ditgneg  24778  lhop1  24935  fta1  25225  ulm2  25301  pilem1  25367  sineq0  25437  ellogrn  25472  rlimcnp  25872  wilthlem1  25974  sqff1o  26088  logfaclbnd  26127  bposlem1  26189  lgsdilem  26229  lgsabs1  26241  lgsdchrval  26259  lgsquadlem1  26285  lgsquadlem2  26286  iscgrgd  26628  trgcgrg  26630  ltgov  26712  ishlg  26717  lnhl  26730  israg  26812  islnopp  26854  iscgra  26924  isinag  26953  iseqlg  26982  nbupgrel  27457  isuvtx  27507  iscplgredg  27529  rusgrnumwwlkl1  28076  clwlkclwwlk2  28110  isclwwlknx  28143  clwwlkn1  28148  nmoo0  28896  ubthlem1  28975  ch0pss  29550  pjnorm2  29832  adjval  29995  leop  30228  atcv0eq  30484  xppreima  30726  fmptcof2  30738  xrdifh  30845  hashgt1  30872  isinftm  31178  lsmsnorb  31317  smatrcl  31484  rhmpreimacnlem  31572  ismntop  31712  brfae  31952  eulerpartlemr  32077  eulerpartlemn  32084  reprinrn  32334  reprinfz1  32338  reprdifc  32343  bnj1173  32718  subfacp1lem5  32882  ttrclselem2  33548  frxp2  33554  xpord2pred  33555  xpord3pred  33561  filnetlem4  34333  bj-clel3gALT  34984  bj-imdirco  35122  taupilem3  35250  topdifinffinlem  35281  finxpsuclem  35331  matunitlindf  35538  poimirlem22  35562  poimirlem26  35566  poimirlem27  35567  heicant  35575  mbfposadd  35587  itg2addnclem  35591  itg2addnclem2  35592  iblabsnclem  35603  ftc1anclem1  35613  ftc1anclem5  35617  areacirclem5  35632  areacirc  35633  lmclim2  35679  caures  35681  rrnheibor  35758  isdmn3  35995  opelvvdif  36161  brxrn  36267  lrelat  36791  lcvbr  36798  lsatcv0eq  36824  ellkr2  36868  lkr0f  36871  lkreqN  36947  opltn0  36967  op1le  36969  leatb  37069  atlltn0  37083  hlrelat5N  37178  hlrelat  37179  cvrval5  37192  cvrexchlem  37196  atcvr0eq  37203  athgt  37233  1cvrco  37249  islpln5  37312  islvol5  37356  elpadd2at2  37584  cdleme0ex2N  38001  cdleme3  38014  cdleme7  38026  cdlemg33e  38487  dochfln0  39254  lcfl1  39269  lcfls1N  39312  lspindp5  39547  isnacs2  40259  rabrenfdioph  40367  rmxycomplete  40470  expdioph  40576  pwfi2f1o  40652  islnr3  40671  isdomn3  40760  sqrtcvallem1  40943  ntrneixb  41410  dffo3f  42418  clim2cf  42894  funressnfv  44237  focofob  44272  oddm1evenALTV  44828  oddp1evenALTV  44829  divgcdoddALTV  44835  ismhm0  45060  isrnghmmul  45152  lco0  45469  lindslinindsimp2lem5  45504  snlindsntor  45513  elbigo2  45599  affinecomb1  45749  itscnhlinecirc02p  45832  iscnrm3lem1  45928
  Copyright terms: Public domain W3C validator