Theorem baib 944

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ 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 197  df-an 386

This theorem is referenced by:  baibr  945  ceqsrexbv  3335  elrab3  3362  dfpss3  3691  rabsn  4254  elrint2  4517  elpredg  5692  fnres  6005  fvmpti  6279  f1ompt  6380  fliftfun  6559  isocnv3  6579  riotaxfrd  6639  ovid  6774  nlimon  7048  limom  7077  brdifun  7768  xpcomco  8047  0sdomg  8086  f1finf1o  8184  ordtypelem9  8428  isacn  8864  alephinit  8915  isfin5-2  9210  pwfseqlem1  9477  pwfseqlem3  9479  pwfseqlem4  9481  ltresr  9958  xrlenlt  10100  znnnlt1  11401  difrp  11865  elfz  12329  fzolb2  12473  elfzo3  12482  fzouzsplit  12499  rabssnn0fi  12780  caubnd  14092  ello12  14241  elo12  14252  bitsval2  15141  smueqlem  15206  rpexp  15426  ramcl  15727  ismon2  16388  isepi2  16395  isfull2  16565  isfth2  16569  isghm3  17655  gastacos  17737  sylow2alem2  18027  lssnle  18081  isabl2  18195  submcmn2  18238  iscyggen2  18277  iscyg3  18282  cyggexb  18294  gsum2d2  18367  dprdw  18403  dprd2da  18435  iscrng2  18557  dvdsr2  18641  dfrhm2  18711  islmhm3  19022  isdomn2  19293  psrbaglefi  19366  mplsubrglem  19433  prmirredlem  19835  chrnzr  19872  iunocv  20019  iscss2  20024  ishil2  20057  obselocv  20066  bastop1  20791  isclo  20885  maxlp  20945  isperf2  20950  restperf  20982  cnpnei  21062  cnntr  21073  cnprest  21087  cnprest2  21088  lmres  21098  iscnrm2  21136  ist0-2  21142  ist1-2  21145  ishaus2  21149  tgcmp  21198  cmpfi  21205  dfconn2  21216  t1connperf  21233  subislly  21278  tx1cn  21406  tx2cn  21407  xkopt  21452  xkoinjcn  21484  ist0-4  21526  trfil2  21685  fin1aufil  21730  flimtopon  21768  elflim  21769  fclstopon  21810  isfcls2  21811  alexsubALTlem4  21848  ptcmplem3  21852  tgphaus  21914  xmetec  22233  prdsbl  22290  blval2  22361  isnvc2  22497  isnghm2  22522  isnmhm2  22550  0nmhm  22553  xrtgioo  22603  cncfcnvcn  22718  evth  22752  nmhmcn  22914  cmsss  23141  lssbn  23142  srabn  23150  ishl2  23160  ivthlem2  23215  0plef  23433  itg2monolem1  23511  itg2cnlem1  23522  itg2cnlem2  23523  ellimc2  23635  dvne0  23768  ellogdm  24379  dcubic  24567  atans2  24652  amgm  24711  ftalem3  24795  pclogsum  24934  dchrelbas3  24957  lgsabs1  25055  dchrvmaeq0  25187  rpvmasum2  25195  ajval  27701  bnsscmcl  27708  axhcompl-zf  27839  seq1hcau  28028  hlim2  28033  issh3  28060  lnopcnre  28882  dmdbr2  29146  elatcv0  29184  iunsnima  29412  1stmbfm  30307  2ndmbfm  30308  eulerpartlemd  30413  oddprm2  30718  cvmlift2lem12  31281  bj-rest10  33025  topdifinfeq  33178  finxpsuclem  33214  curunc  33371  istotbnd2  33549  sstotbnd2  33553  isbnd3b  33564  totbndbnd  33568  islnr2  37510  sdrgacs  37597  areaquad  37628  oddm1evenALTV  41357  oddp1evenALTV  41358