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

Theorem baib 872
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 491 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
2 baib.1 . 2  |-  ( ph  <->  ( ps  /\  ch )
)
31, 2syl6rbbr 256 1  |-  ( ps 
->  ( ph  <->  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  baibr  873  rbaib  874  ceqsrexbv  3006  elrab3  3029  dfpss3  3369  rabsn  3809  elrint2  4027  nlimon  4764  limom  4793  fnres  5494  fvmpti  5737  f1ompt  5823  fliftfun  5966  isocnv3  5984  ovid  6122  riotaxfrd  6510  brdifun  6861  xpcomco  7127  0sdomg  7165  f1finf1o  7264  ordtypelem9  7421  isacn  7851  alephinit  7902  isfin5-2  8197  pwfseqlem1  8459  pwfseqlem3  8461  pwfseqlem4  8463  ltresr  8941  xrlenlt  9069  znnnlt1  10233  difrp  10570  elfz  10974  fzolb2  11069  elfzo3  11078  fzouzsplit  11091  caubnd  12082  ello12  12230  elo12  12241  bitsval2  12857  smueqlem  12922  rpexp  13040  ramcl  13317  ismon2  13880  isepi2  13887  isfull2  14028  isfth2  14032  isghm3  14927  gastacos  15007  sylow2alem2  15172  lssnle  15226  isabl2  15340  submcmn2  15378  iscyggen2  15411  iscyg3  15416  cyggexb  15428  gsum2d2  15468  dprdw  15488  dprd2da  15520  iscrng2  15599  dvdsr2  15672  dfrhm2  15741  islmhm3  16024  isdomn2  16279  psrbaglefi  16357  mplsubrglem  16422  prmirredlem  16689  chrnzr  16727  iunocv  16824  iscss2  16829  ishil2  16862  obselocv  16871  bastop1  16974  isclo  17067  maxlp  17126  isperf2  17131  restperf  17163  cnpnei  17243  cnntr  17254  cnprest  17268  cnprest2  17269  lmres  17279  iscnrm2  17317  ist0-2  17323  ist1-2  17326  ishaus2  17330  tgcmp  17379  cmpfi  17386  dfcon2  17396  t1conperf  17413  subislly  17458  tx1cn  17555  tx2cn  17556  xkopt  17601  xkoinjcn  17633  ist0-4  17675  trfil2  17833  fin1aufil  17878  flimtopon  17916  elflim  17917  fclstopon  17958  isfcls2  17959  alexsubALTlem4  17995  ptcmplem3  17999  tgphaus  18060  xmetec  18347  prdsbl  18404  blval2  18475  isnvc2  18598  isnghm2  18622  isnmhm2  18650  0nmhm  18653  xrtgioo  18701  cncfcnvcn  18815  evth  18848  nmhmcn  18992  cmsss  19165  lssbn  19166  srabn  19174  ishl2  19184  ivthlem2  19209  0plef  19424  itg2monolem1  19502  itg2cnlem1  19513  itg2cnlem2  19514  ellimc2  19624  dvne0  19755  ellogdm  20390  dcubic  20546  atans2  20631  amgm  20689  ftalem3  20717  pclogsum  20859  dchrelbas3  20882  lgsabs1  20978  dchrvmaeq0  21058  rpvmasum2  21066  ajval  22204  bnsscmcl  22211  axhcompl-zf  22342  seq1hcau  22530  hlim2  22535  issh3  22563  lnopcnre  23383  dmdbr2  23647  elatcv0  23685  1stmbfm  24397  2ndmbfm  24398  cvmlift2lem12  24773  elpredg  25195  dffun10  25470  istotbnd2  26163  sstotbnd2  26167  isbnd3b  26178  totbndbnd  26182  islnr2  26980  sdrgacs  27171
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 178  df-an 361
  Copyright terms: Public domain W3C validator