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  2915  elrab3  2937  dfpss3  3275  rabsn  3710  elrint2  3920  nlimon  4658  limom  4687  fnres  5376  fvmpti  5617  f1ompt  5698  fliftfun  5827  isocnv3  5845  ovid  5980  riotaxfrd  6352  brdifun  6703  xpcomco  6968  0sdomg  7006  f1finf1o  7102  ordtypelem9  7257  isacn  7687  alephinit  7738  isfin5-2  8033  pwfseqlem1  8296  pwfseqlem3  8298  pwfseqlem4  8300  ltresr  8778  xrlenlt  8906  znnnlt1  10066  difrp  10403  elfz  10804  fzolb2  10897  elfzo3  10906  fzouzsplit  10917  caubnd  11858  ello12  12006  elo12  12017  bitsval2  12632  sadval  12663  smuval  12688  smueqlem  12697  rpexp  12815  ramcl  13092  ismon2  13653  isepi2  13660  isfull2  13801  isfth2  13805  isghm3  14700  gastacos  14780  sylow2alem2  14945  lssnle  14999  isabl2  15113  submcmn2  15151  iscyggen2  15184  iscyg3  15189  cyggexb  15201  gsum2d2  15241  dprdw  15261  dprd2da  15293  iscrng2  15372  dvdsr2  15445  dfrhm2  15514  islmhm3  15801  isdomn2  16056  psrbaglefi  16134  mplsubrglem  16199  prmirredlem  16462  chrnzr  16500  iunocv  16597  iscss2  16602  ishil2  16635  obselocv  16644  bastop1  16747  isclo  16840  maxlp  16894  isperf2  16899  restperf  16930  cnpnei  17009  cnntr  17020  cnprest  17033  cnprest2  17034  lmres  17044  iscnrm2  17082  ist0-2  17088  ist1-2  17091  ishaus2  17095  tgcmp  17144  cmpfi  17151  dfcon2  17161  t1conperf  17178  subislly  17223  tx1cn  17319  tx2cn  17320  xkopt  17365  xkoinjcn  17397  ist0-4  17436  trfil2  17598  fin1aufil  17643  flimtopon  17681  elflim  17682  fclstopon  17723  isfcls2  17724  alexsubALTlem4  17760  ptcmplem3  17764  tgphaus  17815  xmetec  17996  prdsbl  18053  isnvc2  18225  isnghm2  18249  isnmhm2  18277  0nmhm  18280  xrtgioo  18328  cncfcnvcn  18440  evth  18473  nmhmcn  18617  cmsss  18788  lssbn  18789  srabn  18793  ishl2  18803  ivthlem2  18828  0plef  19043  itg2monolem1  19121  itg2cnlem1  19132  itg2cnlem2  19133  ellimc2  19243  dvne0  19374  ellogdm  20002  dcubic  20158  atans2  20243  amgm  20301  ftalem3  20328  pclogsum  20470  dchrelbas3  20493  lgsabs1  20589  dchrvmaeq0  20669  rpvmasum2  20677  ajval  21456  bnsscmcl  21463  axhcompl-zf  21594  seq1hcau  21782  hlim2  21787  issh3  21815  lnopcnre  22635  dmdbr2  22899  elatcv0  22937  1stmbfm  23580  2ndmbfm  23581  cvmlift2lem12  23860  elpredg  24249  dffun10  24524  dff1o6f  25195  intopcoaconb  25643  intopcoaconc  25644  intcont  25646  prcnt  25654  issubcata  25949  istotbnd2  26597  sstotbnd2  26601  isbnd3b  26612  totbndbnd  26616  islnr2  27421  sdrgacs  27612
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