Theorem baib 525

Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)

Hypothesis

Ref	Expression
baib.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
baib	⊢ (𝜓 → (𝜑 ↔ 𝜒))

Proof of Theorem baib

Step	Hyp	Ref	Expression
1		ibar 518	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
2		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	1, 2	syl6rbbr 279	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 383

This theorem is referenced by:  baibr  526  ceqsrexbv  3487  elrab3  3516  dfpss3  3843  rabsn  4392  elrint2  4653  elpredg  5835  fnres  6145  fvmpti  6421  f1ompt  6522  fliftfun  6703  isocnv3  6723  riotaxfrd  6783  ovid  6922  nlimon  7196  limom  7225  brdifun  7923  xpcomco  8204  0sdomg  8243  f1finf1o  8341  ordtypelem9  8585  isacn  9065  alephinit  9116  isfin5-2  9413  pwfseqlem1  9680  pwfseqlem3  9682  pwfseqlem4  9684  ltresr  10161  xrlenlt  10303  znnnlt1  11604  difrp  12064  elfz  12532  fzolb2  12678  elfzo3  12687  fzouzsplit  12704  rabssnn0fi  12986  caubnd  14299  ello12  14448  elo12  14459  bitsval2  15348  smueqlem  15413  rpexp  15632  ramcl  15933  ismon2  16594  isepi2  16601  isfull2  16771  isfth2  16775  isghm3  17862  gastacos  17943  sylow2alem2  18233  lssnle  18287  isabl2  18401  submcmn2  18444  iscyggen2  18483  iscyg3  18488  cyggexb  18500  gsum2d2  18573  dprdw  18610  dprd2da  18642  iscrng2  18764  dvdsr2  18848  dfrhm2  18920  islmhm3  19234  isdomn2  19507  psrbaglefi  19580  mplsubrglem  19647  prmirredlem  20049  chrnzr  20086  iunocv  20235  iscss2  20240  ishil2  20273  obselocv  20282  bastop1  21011  isclo  21105  maxlp  21165  isperf2  21170  restperf  21202  cnpnei  21282  cnntr  21293  cnprest  21307  cnprest2  21308  lmres  21318  iscnrm2  21356  ist0-2  21362  ist1-2  21365  ishaus2  21369  tgcmp  21418  cmpfi  21425  dfconn2  21436  t1connperf  21453  subislly  21498  tx1cn  21626  tx2cn  21627  xkopt  21672  xkoinjcn  21704  ist0-4  21746  trfil2  21904  fin1aufil  21949  flimtopon  21987  elflim  21988  fclstopon  22029  isfcls2  22030  alexsubALTlem4  22067  ptcmplem3  22071  tgphaus  22133  xmetec  22452  prdsbl  22509  blval2  22580  isnvc2  22716  isnghm2  22741  isnmhm2  22769  0nmhm  22772  xrtgioo  22822  cncfcnvcn  22937  evth  22971  nmhmcn  23132  cmsss  23359  lssbn  23360  srabn  23368  ishl2  23378  ivthlem2  23433  0plef  23652  itg2monolem1  23730  itg2cnlem1  23741  itg2cnlem2  23742  ellimc2  23854  dvne0  23987  ellogdm  24599  dcubic  24787  atans2  24872  amgm  24931  ftalem3  25015  pclogsum  25154  dchrelbas3  25177  lgsabs1  25275  dchrvmaeq0  25407  rpvmasum2  25415  clwwlkwwlksb  27204  ajval  28050  bnsscmcl  28057  axhcompl-zf  28188  seq1hcau  28377  hlim2  28382  issh3  28409  lnopcnre  29231  dmdbr2  29495  elatcv0  29533  iunsnima  29761  1stmbfm  30655  2ndmbfm  30656  eulerpartlemd  30761  oddprm2  31066  cvmlift2lem12  31627  bj-rest10  33366  topdifinfeq  33528  finxpsuclem  33564  curunc  33717  istotbnd2  33894  sstotbnd2  33898  isbnd3b  33909  totbndbnd  33913  ecres2  34380  islnr2  38203  sdrgacs  38290  areaquad  38321  oddm1evenALTV  42107  oddp1evenALTV  42108