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  5837  fnres  6147  fvmpti  6423  f1ompt  6524  fliftfun  6705  isocnv3  6725  riotaxfrd  6785  ovid  6924  nlimon  7198  limom  7227  brdifun  7925  xpcomco  8206  0sdomg  8245  f1finf1o  8343  ordtypelem9  8587  isacn  9067  alephinit  9118  isfin5-2  9415  pwfseqlem1  9682  pwfseqlem3  9684  pwfseqlem4  9686  ltresr  10163  xrlenlt  10305  znnnlt1  11606  difrp  12071  elfz  12539  fzolb2  12685  elfzo3  12694  fzouzsplit  12711  rabssnn0fi  12993  caubnd  14306  ello12  14455  elo12  14466  bitsval2  15355  smueqlem  15420  rpexp  15639  ramcl  15940  ismon2  16601  isepi2  16608  isfull2  16778  isfth2  16782  isghm3  17869  gastacos  17950  sylow2alem2  18240  lssnle  18294  isabl2  18408  submcmn2  18451  iscyggen2  18490  iscyg3  18495  cyggexb  18507  gsum2d2  18580  dprdw  18617  dprd2da  18649  iscrng2  18771  dvdsr2  18855  dfrhm2  18927  islmhm3  19241  isdomn2  19514  psrbaglefi  19587  mplsubrglem  19654  prmirredlem  20056  chrnzr  20093  iunocv  20242  iscss2  20247  ishil2  20280  obselocv  20289  bastop1  21018  isclo  21112  maxlp  21172  isperf2  21177  restperf  21209  cnpnei  21289  cnntr  21300  cnprest  21314  cnprest2  21315  lmres  21325  iscnrm2  21363  ist0-2  21369  ist1-2  21372  ishaus2  21376  tgcmp  21425  cmpfi  21432  dfconn2  21443  t1connperf  21460  subislly  21505  tx1cn  21633  tx2cn  21634  xkopt  21679  xkoinjcn  21711  ist0-4  21753  trfil2  21911  fin1aufil  21956  flimtopon  21994  elflim  21995  fclstopon  22036  isfcls2  22037  alexsubALTlem4  22074  ptcmplem3  22078  tgphaus  22140  xmetec  22459  prdsbl  22516  blval2  22587  isnvc2  22723  isnghm2  22748  isnmhm2  22776  0nmhm  22779  xrtgioo  22829  cncfcnvcn  22944  evth  22978  nmhmcn  23139  cmsss  23366  lssbn  23367  srabn  23375  ishl2  23385  ivthlem2  23440  0plef  23659  itg2monolem1  23737  itg2cnlem1  23748  itg2cnlem2  23749  ellimc2  23861  dvne0  23994  ellogdm  24606  dcubic  24794  atans2  24879  amgm  24938  ftalem3  25022  pclogsum  25161  dchrelbas3  25184  lgsabs1  25282  dchrvmaeq0  25414  rpvmasum2  25422  clwwlkwwlksb  27211  ajval  28057  bnsscmcl  28064  axhcompl-zf  28195  seq1hcau  28384  hlim2  28389  issh3  28416  lnopcnre  29238  dmdbr2  29502  elatcv0  29540  iunsnima  29768  1stmbfm  30662  2ndmbfm  30663  eulerpartlemd  30768  oddprm2  31073  cvmlift2lem12  31634  bj-rest10  33373  topdifinfeq  33535  finxpsuclem  33571  curunc  33724  istotbnd2  33901  sstotbnd2  33905  isbnd3b  33916  totbndbnd  33920  ecres2  34387  islnr2  38210  sdrgacs  38297  areaquad  38328  oddm1evenALTV  42114  oddp1evenALTV  42115