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

Theorem baib 871
Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
Hypothesis
Ref Expression
baib.1  |-  ( ph  <->  ( ps  /\  ch )
)
Assertion
Ref Expression
baib  |-  ( ps 
->  ( ph  <->  ch )
)

Proof of Theorem baib
StepHypRef Expression
1 ibar 490 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
2 baib.1 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
31, 2syl6rbbr 255 1  |-  ( ps 
->  ( ph  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  baibr  872  rbaib  873  ceqsrexbv  2902  elrab3  2924  dfpss3  3262  rabsn  3697  elrint2  3904  nlimon  4642  limom  4671  fnres  5360  fvmpti  5601  f1ompt  5682  fliftfun  5811  isocnv3  5829  ovid  5964  riotaxfrd  6336  brdifun  6687  xpcomco  6952  0sdomg  6990  f1finf1o  7086  ordtypelem9  7241  isacn  7671  alephinit  7722  isfin5-2  8017  pwfseqlem1  8280  pwfseqlem3  8282  pwfseqlem4  8284  ltresr  8762  xrlenlt  8890  znnnlt1  10050  difrp  10387  elfz  10788  fzolb2  10881  elfzo3  10890  fzouzsplit  10901  caubnd  11842  ello12  11990  elo12  12001  bitsval2  12616  sadval  12647  smuval  12672  smueqlem  12681  rpexp  12799  ramcl  13076  ismon2  13637  isepi2  13644  isfull2  13785  isfth2  13789  isghm3  14684  gastacos  14764  sylow2alem2  14929  lssnle  14983  isabl2  15097  submcmn2  15135  iscyggen2  15168  iscyg3  15173  cyggexb  15185  gsum2d2  15225  dprdw  15245  dprd2da  15277  iscrng2  15356  dvdsr2  15429  dfrhm2  15498  islmhm3  15785  isdomn2  16040  psrbaglefi  16118  mplsubrglem  16183  prmirredlem  16446  chrnzr  16484  iunocv  16581  iscss2  16586  ishil2  16619  obselocv  16628  bastop1  16731  isclo  16824  maxlp  16878  isperf2  16883  restperf  16914  cnpnei  16993  cnntr  17004  cnprest  17017  cnprest2  17018  lmres  17028  iscnrm2  17066  ist0-2  17072  ist1-2  17075  ishaus2  17079  tgcmp  17128  cmpfi  17135  dfcon2  17145  t1conperf  17162  subislly  17207  tx1cn  17303  tx2cn  17304  xkopt  17349  xkoinjcn  17381  ist0-4  17420  trfil2  17582  fin1aufil  17627  flimtopon  17665  elflim  17666  fclstopon  17707  isfcls2  17708  alexsubALTlem4  17744  ptcmplem3  17748  tgphaus  17799  xmetec  17980  prdsbl  18037  isnvc2  18209  isnghm2  18233  isnmhm2  18261  0nmhm  18264  xrtgioo  18312  cncfcnvcn  18424  evth  18457  nmhmcn  18601  cmsss  18772  lssbn  18773  srabn  18777  ishl2  18787  ivthlem2  18812  0plef  19027  itg2monolem1  19105  itg2cnlem1  19116  itg2cnlem2  19117  ellimc2  19227  dvne0  19358  ellogdm  19986  dcubic  20142  atans2  20227  amgm  20285  ftalem3  20312  pclogsum  20454  dchrelbas3  20477  lgsabs1  20573  dchrvmaeq0  20653  rpvmasum2  20661  ajval  21440  bnsscmcl  21447  axhcompl-zf  21578  seq1hcau  21766  hlim2  21771  issh3  21799  lnopcnre  22619  dmdbr2  22883  elatcv0  22921  1stmbfm  23565  2ndmbfm  23566  cvmlift2lem12  23845  elpredg  24178  dffun10  24453  dff1o6f  25092  intopcoaconb  25540  intopcoaconc  25541  intcont  25543  prcnt  25551  issubcata  25846  istotbnd2  26494  sstotbnd2  26498  isbnd3b  26509  totbndbnd  26513  islnr2  27318  sdrgacs  27509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator