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  3038  elrab3  3061  dfpss3  3401  rabsn  3841  elrint2  4060  nlimon  4798  limom  4827  fnres  5528  fvmpti  5772  f1ompt  5858  fliftfun  6001  isocnv3  6019  ovid  6157  riotaxfrd  6548  brdifun  6899  xpcomco  7165  0sdomg  7203  f1finf1o  7302  ordtypelem9  7459  isacn  7889  alephinit  7940  isfin5-2  8235  pwfseqlem1  8497  pwfseqlem3  8499  pwfseqlem4  8501  ltresr  8979  xrlenlt  9107  znnnlt1  10272  difrp  10609  elfz  11013  fzolb2  11109  elfzo3  11118  fzouzsplit  11131  caubnd  12125  ello12  12273  elo12  12284  bitsval2  12900  smueqlem  12965  rpexp  13083  ramcl  13360  ismon2  13923  isepi2  13930  isfull2  14071  isfth2  14075  isghm3  14970  gastacos  15050  sylow2alem2  15215  lssnle  15269  isabl2  15383  submcmn2  15421  iscyggen2  15454  iscyg3  15459  cyggexb  15471  gsum2d2  15511  dprdw  15531  dprd2da  15563  iscrng2  15642  dvdsr2  15715  dfrhm2  15784  islmhm3  16067  isdomn2  16322  psrbaglefi  16400  mplsubrglem  16465  prmirredlem  16736  chrnzr  16774  iunocv  16871  iscss2  16876  ishil2  16909  obselocv  16918  bastop1  17021  isclo  17114  maxlp  17173  isperf2  17178  restperf  17210  cnpnei  17290  cnntr  17301  cnprest  17315  cnprest2  17316  lmres  17326  iscnrm2  17364  ist0-2  17370  ist1-2  17373  ishaus2  17377  tgcmp  17426  cmpfi  17433  dfcon2  17443  t1conperf  17460  subislly  17505  tx1cn  17602  tx2cn  17603  xkopt  17648  xkoinjcn  17680  ist0-4  17722  trfil2  17880  fin1aufil  17925  flimtopon  17963  elflim  17964  fclstopon  18005  isfcls2  18006  alexsubALTlem4  18042  ptcmplem3  18046  tgphaus  18107  xmetec  18425  prdsbl  18482  blval2  18566  isnvc2  18695  isnghm2  18719  isnmhm2  18747  0nmhm  18750  xrtgioo  18798  cncfcnvcn  18912  evth  18945  nmhmcn  19089  cmsss  19264  lssbn  19265  srabn  19275  ishl2  19285  ivthlem2  19310  0plef  19525  itg2monolem1  19603  itg2cnlem1  19614  itg2cnlem2  19615  ellimc2  19725  dvne0  19856  ellogdm  20491  dcubic  20647  atans2  20732  amgm  20790  ftalem3  20818  pclogsum  20960  dchrelbas3  20983  lgsabs1  21079  dchrvmaeq0  21159  rpvmasum2  21167  ajval  22324  bnsscmcl  22331  axhcompl-zf  22462  seq1hcau  22650  hlim2  22655  issh3  22683  lnopcnre  23503  dmdbr2  23767  elatcv0  23805  isarchi  24213  1stmbfm  24571  2ndmbfm  24572  cvmlift2lem12  24962  elpredg  25400  dffun10  25675  istotbnd2  26377  sstotbnd2  26381  isbnd3b  26392  totbndbnd  26396  islnr2  27194  sdrgacs  27385
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