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

Theorem baib 943
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
Hypothesis
Ref Expression
baib.1 (𝜑 ↔ (𝜓𝜒))
Assertion
Ref Expression
baib (𝜓 → (𝜑𝜒))

Proof of Theorem baib
StepHypRef Expression
1 ibar 525 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
2 baib.1 . 2 (𝜑 ↔ (𝜓𝜒))
31, 2syl6rbbr 279 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  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 197  df-an 386
This theorem is referenced by:  baibr  944  ceqsrexbv  3321  elrab3  3348  dfpss3  3673  rabsn  4228  elrint2  4486  elpredg  5655  fnres  5967  fvmpti  6240  f1ompt  6340  fliftfun  6519  isocnv3  6539  riotaxfrd  6599  ovid  6733  nlimon  7001  limom  7030  brdifun  7719  xpcomco  7997  0sdomg  8036  f1finf1o  8134  ordtypelem9  8378  isacn  8814  alephinit  8865  isfin5-2  9160  pwfseqlem1  9427  pwfseqlem3  9429  pwfseqlem4  9431  ltresr  9908  xrlenlt  10050  znnnlt1  11351  difrp  11815  elfz  12277  fzolb2  12421  elfzo3  12430  fzouzsplit  12447  rabssnn0fi  12728  caubnd  14035  ello12  14184  elo12  14195  bitsval2  15074  smueqlem  15139  rpexp  15359  ramcl  15660  ismon2  16318  isepi2  16325  isfull2  16495  isfth2  16499  isghm3  17585  gastacos  17667  sylow2alem2  17957  lssnle  18011  isabl2  18125  submcmn2  18168  iscyggen2  18207  iscyg3  18212  cyggexb  18224  gsum2d2  18297  dprdw  18333  dprd2da  18365  iscrng2  18487  dvdsr2  18571  dfrhm2  18641  islmhm3  18950  isdomn2  19221  psrbaglefi  19294  mplsubrglem  19361  prmirredlem  19763  chrnzr  19800  iunocv  19947  iscss2  19952  ishil2  19985  obselocv  19994  bastop1  20711  isclo  20804  maxlp  20864  isperf2  20869  restperf  20901  cnpnei  20981  cnntr  20992  cnprest  21006  cnprest2  21007  lmres  21017  iscnrm2  21055  ist0-2  21061  ist1-2  21064  ishaus2  21068  tgcmp  21117  cmpfi  21124  dfconn2  21135  t1connperf  21152  subislly  21197  tx1cn  21325  tx2cn  21326  xkopt  21371  xkoinjcn  21403  ist0-4  21445  trfil2  21604  fin1aufil  21649  flimtopon  21687  elflim  21688  fclstopon  21729  isfcls2  21730  alexsubALTlem4  21767  ptcmplem3  21771  tgphaus  21833  xmetec  22152  prdsbl  22209  blval2  22280  isnvc2  22416  isnghm2  22441  isnmhm2  22469  0nmhm  22472  xrtgioo  22522  cncfcnvcn  22637  evth  22671  nmhmcn  22833  cmsss  23060  lssbn  23061  srabn  23069  ishl2  23079  ivthlem2  23134  0plef  23352  itg2monolem1  23430  itg2cnlem1  23441  itg2cnlem2  23442  ellimc2  23554  dvne0  23685  ellogdm  24292  dcubic  24480  atans2  24565  amgm  24624  ftalem3  24708  pclogsum  24847  dchrelbas3  24870  lgsabs1  24968  dchrvmaeq0  25100  rpvmasum2  25108  ajval  27578  bnsscmcl  27585  axhcompl-zf  27716  seq1hcau  27905  hlim2  27910  issh3  27937  lnopcnre  28759  dmdbr2  29023  elatcv0  29061  iunsnima  29283  1stmbfm  30115  2ndmbfm  30116  eulerpartlemd  30221  cvmlift2lem12  31025  bj-rest10  32699  topdifinfeq  32851  finxpsuclem  32887  curunc  33044  istotbnd2  33222  sstotbnd2  33226  isbnd3b  33237  totbndbnd  33241  islnr2  37186  sdrgacs  37273  areaquad  37304  oddm1evenALTV  40901  oddp1evenALTV  40902
  Copyright terms: Public domain W3C validator