Theorem baib 535

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		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2		ibar 528	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	bitr4id 290	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  baibr  536  ceqsrexbv  3656  elrab3  3693  dfpss3  4089  rabsn  4721  elrint2  4990  opres  6007  cores  6269  fnres  6695  fvres  6925  fvmpti  7015  f1ompt  7131  fliftfun  7332  isocnv3  7352  riotaxfrd  7422  ovid  7574  nlimon  7872  limom  7903  brdifun  8775  xpcomco  9102  0sdomg  9144  0sdomgOLD  9145  f1finf1o  9305  f1finf1oOLD  9306  ordtypelem9  9566  isacn  10084  alephinit  10135  isfin5-2  10431  pwfseqlem1  10698  pwfseqlem3  10700  pwfseqlem4  10702  ltresr  11180  xrlenlt  11326  znnnlt1  12644  difrp  13073  elfz  13553  fzolb2  13706  elfzo3  13716  fzouzsplit  13734  rabssnn0fi  14027  caubnd  15397  ello12  15552  elo12  15563  bitsval2  16462  smueqlem  16527  rpexp  16759  ramcl  17067  ismon2  17778  isepi2  17785  isfull2  17958  isfth2  17962  isghm3  19235  gastacos  19328  sylow2alem2  19636  lssnle  19692  isabl2  19808  submcmn2  19857  iscyggen2  19899  iscyg3  19904  cyggexb  19917  gsum2d2  19992  dprdw  20030  dprd2da  20062  iscrng2  20249  dvdsr2  20363  dfrhm2  20474  isdomn2  20711  isdomn2OLD  20712  sdrgacs  20802  islmhm3  21027  prmirredlem  21483  chrnzr  21545  iunocv  21699  iscss2  21704  ishil2  21739  obselocv  21748  psrbaglefi  21946  mplsubrglem  22024  bastop1  23000  isclo  23095  maxlp  23155  isperf2  23160  restperf  23192  cnpnei  23272  cnntr  23283  cnprest  23297  cnprest2  23298  lmres  23308  iscnrm2  23346  ist0-2  23352  ist1-2  23355  ishaus2  23359  tgcmp  23409  cmpfi  23416  dfconn2  23427  t1connperf  23444  subislly  23489  tx1cn  23617  tx2cn  23618  xkopt  23663  xkoinjcn  23695  ist0-4  23737  trfil2  23895  fin1aufil  23940  flimtopon  23978  elflim  23979  fclstopon  24020  isfcls2  24021  alexsubALTlem4  24058  ptcmplem3  24062  tgphaus  24125  xmetec  24444  prdsbl  24504  blval2  24575  isnvc2  24720  isnghm2  24745  isnmhm2  24773  0nmhm  24776  xrtgioo  24828  cncfcnvcn  24952  evth  24991  nmhmcn  25153  cmsss  25385  lssbn  25386  srabn  25394  ishl2  25404  ivthlem2  25487  0plef  25707  itg2monolem1  25785  itg2cnlem1  25796  itg2cnlem2  25797  ellimc2  25912  dvne0  26050  ellogdm  26681  dcubic  26889  atans2  26974  amgm  27034  ftalem3  27118  pclogsum  27259  dchrelbas3  27282  lgsabs1  27380  dchrvmaeq0  27548  rpvmasum2  27556  tgjustf  28481  clwwlkwwlksb  30073  ajval  30880  bnsscmcl  30887  axhcompl-zf  31017  seq1hcau  31206  hlim2  31211  issh3  31238  lnopcnre  32058  dmdbr2  32322  elatcv0  32360  iunsnima  32630  iunsnima2  32631  ecxpid  33389  ssdifidlprm  33486  ist0cld  33832  1stmbfm  34262  2ndmbfm  34263  eulerpartlemd  34368  oddprm2  34670  lfuhgr  35123  cvmlift2lem12  35319  bj-rest10  37089  topdifinfeq  37351  finxpsuclem  37398  curunc  37609  istotbnd2  37777  sstotbnd2  37781  isbnd3b  37792  totbndbnd  37796  br1cnvres  38270  ecres2  38280  fimgmcyc  42544  islnr2  43126  areaquad  43228  tfsconcat0i  43358  afv2res  47251  oddm1evenALTV  47662  oddp1evenALTV  47663  iscnrm3v  48850  isprsd  48852  joindm2  48865  meetdm2  48867  postcposALT  49172  postc  49173