MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  baib Structured version   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  3070  elrab3  3093  dfpss3  3433  rabsn  3873  elrint2  4092  nlimon  4831  limom  4860  fnres  5561  fvmpti  5805  f1ompt  5891  fliftfun  6034  isocnv3  6052  ovid  6190  riotaxfrd  6581  brdifun  6932  xpcomco  7198  0sdomg  7236  f1finf1o  7335  ordtypelem9  7495  isacn  7925  alephinit  7976  isfin5-2  8271  pwfseqlem1  8533  pwfseqlem3  8535  pwfseqlem4  8537  ltresr  9015  xrlenlt  9143  znnnlt1  10308  difrp  10645  elfz  11049  fzolb2  11146  elfzo3  11155  fzouzsplit  11168  caubnd  12162  ello12  12310  elo12  12321  bitsval2  12937  smueqlem  13002  rpexp  13120  ramcl  13397  ismon2  13960  isepi2  13967  isfull2  14108  isfth2  14112  isghm3  15007  gastacos  15087  sylow2alem2  15252  lssnle  15306  isabl2  15420  submcmn2  15458  iscyggen2  15491  iscyg3  15496  cyggexb  15508  gsum2d2  15548  dprdw  15568  dprd2da  15600  iscrng2  15679  dvdsr2  15752  dfrhm2  15821  islmhm3  16104  isdomn2  16359  psrbaglefi  16437  mplsubrglem  16502  prmirredlem  16773  chrnzr  16811  iunocv  16908  iscss2  16913  ishil2  16946  obselocv  16955  bastop1  17058  isclo  17151  maxlp  17211  isperf2  17216  restperf  17248  cnpnei  17328  cnntr  17339  cnprest  17353  cnprest2  17354  lmres  17364  iscnrm2  17402  ist0-2  17408  ist1-2  17411  ishaus2  17415  tgcmp  17464  cmpfi  17471  dfcon2  17482  t1conperf  17499  subislly  17544  tx1cn  17641  tx2cn  17642  xkopt  17687  xkoinjcn  17719  ist0-4  17761  trfil2  17919  fin1aufil  17964  flimtopon  18002  elflim  18003  fclstopon  18044  isfcls2  18045  alexsubALTlem4  18081  ptcmplem3  18085  tgphaus  18146  xmetec  18464  prdsbl  18521  blval2  18605  isnvc2  18734  isnghm2  18758  isnmhm2  18786  0nmhm  18789  xrtgioo  18837  cncfcnvcn  18951  evth  18984  nmhmcn  19128  cmsss  19303  lssbn  19304  srabn  19314  ishl2  19324  ivthlem2  19349  0plef  19564  itg2monolem1  19642  itg2cnlem1  19653  itg2cnlem2  19654  ellimc2  19764  dvne0  19895  ellogdm  20530  dcubic  20686  atans2  20771  amgm  20829  ftalem3  20857  pclogsum  20999  dchrelbas3  21022  lgsabs1  21118  dchrvmaeq0  21198  rpvmasum2  21206  ajval  22363  bnsscmcl  22370  axhcompl-zf  22501  seq1hcau  22689  hlim2  22694  issh3  22722  lnopcnre  23542  dmdbr2  23806  elatcv0  23844  isarchi  24252  1stmbfm  24610  2ndmbfm  24611  cvmlift2lem12  25001  elpredg  25453  istotbnd2  26479  sstotbnd2  26483  isbnd3b  26494  totbndbnd  26498  islnr2  27295  sdrgacs  27486
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