Theorem baib 527

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 520	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
2		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	1, 2	syl6rbbr 281	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  baibr  528  ceqsrexbv  3531  elrab3  3560  dfpss3  3891  rabsn  4447  elrint2  4711  elpredg  5907  fnres  6214  fvmpti  6498  f1ompt  6599  fliftfun  6782  isocnv3  6802  riotaxfrd  6862  ovid  7003  nlimon  7277  limom  7306  brdifun  8004  xpcomco  8285  0sdomg  8324  f1finf1o  8422  ordtypelem9  8666  isacn  9146  alephinit  9197  isfin5-2  9494  pwfseqlem1  9761  pwfseqlem3  9763  pwfseqlem4  9765  ltresr  10242  xrlenlt  10384  znnnlt1  11666  difrp  12078  elfz  12551  fzolb2  12697  elfzo3  12706  fzouzsplit  12723  rabssnn0fi  13005  caubnd  14317  ello12  14466  elo12  14477  bitsval2  15362  smueqlem  15427  rpexp  15645  ramcl  15946  ismon2  16594  isepi2  16601  isfull2  16771  isfth2  16775  isghm3  17859  gastacos  17940  sylow2alem2  18230  lssnle  18284  isabl2  18398  submcmn2  18441  iscyggen2  18480  iscyg3  18485  cyggexb  18497  gsum2d2  18570  dprdw  18607  dprd2da  18639  iscrng2  18761  dvdsr2  18845  dfrhm2  18917  islmhm3  19231  isdomn2  19504  psrbaglefi  19577  mplsubrglem  19644  prmirredlem  20045  chrnzr  20082  iunocv  20232  iscss2  20237  ishil2  20270  obselocv  20279  bastop1  21008  isclo  21102  maxlp  21162  isperf2  21167  restperf  21199  cnpnei  21279  cnntr  21290  cnprest  21304  cnprest2  21305  lmres  21315  iscnrm2  21353  ist0-2  21359  ist1-2  21362  ishaus2  21366  tgcmp  21415  cmpfi  21422  dfconn2  21433  t1connperf  21450  subislly  21495  tx1cn  21623  tx2cn  21624  xkopt  21669  xkoinjcn  21701  ist0-4  21743  trfil2  21901  fin1aufil  21946  flimtopon  21984  elflim  21985  fclstopon  22026  isfcls2  22027  alexsubALTlem4  22064  ptcmplem3  22068  tgphaus  22130  xmetec  22449  prdsbl  22506  blval2  22577  isnvc2  22713  isnghm2  22738  isnmhm2  22766  0nmhm  22769  xrtgioo  22819  cncfcnvcn  22934  evth  22968  nmhmcn  23129  cmsss  23357  lssbn  23358  srabn  23366  ishl2  23376  ivthlem2  23432  0plef  23652  itg2monolem1  23730  itg2cnlem1  23741  itg2cnlem2  23742  ellimc2  23854  dvne0  23987  ellogdm  24598  dcubic  24786  atans2  24871  amgm  24930  ftalem3  25014  pclogsum  25153  dchrelbas3  25176  lgsabs1  25274  dchrvmaeq0  25406  rpvmasum2  25414  clwwlkwwlksb  27203  ajval  28044  bnsscmcl  28051  axhcompl-zf  28182  seq1hcau  28371  hlim2  28376  issh3  28403  lnopcnre  29225  dmdbr2  29489  elatcv0  29527  iunsnima  29754  1stmbfm  30646  2ndmbfm  30647  eulerpartlemd  30752  oddprm2  31057  cvmlift2lem12  31617  bj-rest10  33350  topdifinfeq  33512  finxpsuclem  33548  curunc  33702  istotbnd2  33878  sstotbnd2  33882  isbnd3b  33893  totbndbnd  33897  ecres2  34359  islnr2  38182  sdrgacs  38269  areaquad  38299  oddm1evenALTV  42158  oddp1evenALTV  42159