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

Theorem baib 903
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 504 . 2
2 baib.1 . 2
31, 2syl6rbbr 264 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  baibr  904  rbaibOLD  907  ceqsrexbv  3234  elrab3  3258  dfpss3  3589  rabsn  4097  elrint2  4329  fnres  5702  fvmpti  5955  f1ompt  6053  fliftfun  6210  isocnv3  6228  riotaxfrd  6288  ovid  6419  nlimon  6686  limom  6715  brdifun  7357  xpcomco  7627  0sdomg  7666  f1finf1o  7766  ordtypelem9  7972  isacn  8446  alephinit  8497  isfin5-2  8792  pwfseqlem1  9057  pwfseqlem3  9059  pwfseqlem4  9061  ltresr  9538  xrlenlt  9673  znnnlt1  10916  difrp  11282  elfz  11707  fzolb2  11835  elfzo3  11844  fzouzsplit  11860  rabssnn0fi  12095  caubnd  13191  ello12  13339  elo12  13350  bitsval2  14075  smueqlem  14140  rpexp  14261  ramcl  14547  ismon2  15129  isepi2  15136  isfull2  15280  isfth2  15284  isghm3  16268  gastacos  16348  sylow2alem2  16638  lssnle  16692  isabl2  16806  submcmn2  16847  iscyggen2  16884  iscyg3  16889  cyggexb  16901  gsum2d2  17002  dprdw  17043  dprdwOLD  17050  dprd2da  17091  iscrng2  17214  dvdsr2  17296  dfrhm2  17366  islmhm3  17674  isdomn2  17948  psrbaglefi  18023  psrbaglefiOLD  18024  mplsubrglem  18100  mplsubrglemOLD  18101  prmirredlem  18523  prmirredlemOLD  18526  chrnzr  18567  iunocv  18712  iscss2  18717  ishil2  18750  obselocv  18759  bastop1  19495  isclo  19588  maxlp  19648  isperf2  19653  restperf  19685  cnpnei  19765  cnntr  19776  cnprest  19790  cnprest2  19791  lmres  19801  iscnrm2  19839  ist0-2  19845  ist1-2  19848  ishaus2  19852  tgcmp  19901  cmpfi  19908  dfcon2  19920  t1conperf  19937  subislly  19982  tx1cn  20110  tx2cn  20111  xkopt  20156  xkoinjcn  20188  ist0-4  20230  trfil2  20388  fin1aufil  20433  flimtopon  20471  elflim  20472  fclstopon  20513  isfcls2  20514  alexsubALTlem4  20550  ptcmplem3  20554  tgphaus  20615  xmetec  20937  prdsbl  20994  blval2  21078  isnvc2  21207  isnghm2  21231  isnmhm2  21259  0nmhm  21262  xrtgioo  21311  cncfcnvcn  21425  evth  21459  nmhmcn  21603  cmsss  21789  lssbn  21790  srabn  21800  ishl2  21810  ivthlem2  21864  0plef  22079  itg2monolem1  22157  itg2cnlem1  22168  itg2cnlem2  22169  ellimc2  22281  dvne0  22412  ellogdm  23020  dcubic  23177  atans2  23262  amgm  23320  ftalem3  23348  pclogsum  23490  dchrelbas3  23513  lgsabs1  23609  dchrvmaeq0  23689  rpvmasum2  23697  ajval  25777  bnsscmcl  25784  axhcompl-zf  25915  seq1hcau  26104  hlim2  26109  issh3  26137  lnopcnre  26958  dmdbr2  27222  elatcv0  27260  1stmbfm  28231  2ndmbfm  28232  eulerpartlemd  28305  cvmlift2lem12  28759  elpredg  29258  istotbnd2  30266  sstotbnd2  30270  isbnd3b  30281  totbndbnd  30285  islnr2  31063  sdrgacs  31150  areaquad  31184
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 185  df-an 371
  Copyright terms: Public domain W3C validator