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  3622  elrab3  3660  dfpss3  4052  rabsn  4685  elrint2  4954  opres  5960  cores  6222  fnres  6645  fvres  6877  fvmpti  6967  f1ompt  7083  fliftfun  7287  isocnv3  7307  riotaxfrd  7378  ovid  7530  nlimon  7827  limom  7858  brdifun  8701  elecreseq  8720  xpcomco  9031  0sdomg  9070  f1finf1o  9216  f1finf1oOLD  9217  ordtypelem9  9479  isacn  9997  alephinit  10048  isfin5-2  10344  pwfseqlem1  10611  pwfseqlem3  10613  pwfseqlem4  10615  ltresr  11093  xrlenlt  11239  znnnlt1  12560  difrp  12991  elfz  13474  fzolb2  13627  elfzo3  13637  fzouzsplit  13655  rabssnn0fi  13951  caubnd  15325  ello12  15482  elo12  15493  bitsval2  16395  smueqlem  16460  rpexp  16692  ramcl  17000  ismon2  17696  isepi2  17703  isfull2  17875  isfth2  17879  isghm3  19149  gastacos  19242  sylow2alem2  19548  lssnle  19604  isabl2  19720  submcmn2  19769  iscyggen2  19811  iscyg3  19816  cyggexb  19829  gsum2d2  19904  dprdw  19942  dprd2da  19974  iscrng2  20161  dvdsr2  20272  dfrhm2  20383  isdomn2  20620  isdomn2OLD  20621  sdrgacs  20710  islmhm3  20935  prmirredlem  21382  chrnzr  21440  iunocv  21590  iscss2  21595  ishil2  21628  obselocv  21637  psrbaglefi  21835  mplsubrglem  21913  bastop1  22880  isclo  22974  maxlp  23034  isperf2  23039  restperf  23071  cnpnei  23151  cnntr  23162  cnprest  23176  cnprest2  23177  lmres  23187  iscnrm2  23225  ist0-2  23231  ist1-2  23234  ishaus2  23238  tgcmp  23288  cmpfi  23295  dfconn2  23306  t1connperf  23323  subislly  23368  tx1cn  23496  tx2cn  23497  xkopt  23542  xkoinjcn  23574  ist0-4  23616  trfil2  23774  fin1aufil  23819  flimtopon  23857  elflim  23858  fclstopon  23899  isfcls2  23900  alexsubALTlem4  23937  ptcmplem3  23941  tgphaus  24004  xmetec  24322  prdsbl  24379  blval2  24450  isnvc2  24587  isnghm2  24612  isnmhm2  24640  0nmhm  24643  xrtgioo  24695  cncfcnvcn  24819  evth  24858  nmhmcn  25020  cmsss  25251  lssbn  25252  srabn  25260  ishl2  25270  ivthlem2  25353  0plef  25573  itg2monolem1  25651  itg2cnlem1  25662  itg2cnlem2  25663  ellimc2  25778  dvne0  25916  ellogdm  26548  dcubic  26756  atans2  26841  amgm  26901  ftalem3  26985  pclogsum  27126  dchrelbas3  27149  lgsabs1  27247  dchrvmaeq0  27415  rpvmasum2  27423  tgjustf  28400  clwwlkwwlksb  29983  ajval  30790  bnsscmcl  30797  axhcompl-zf  30927  seq1hcau  31116  hlim2  31121  issh3  31148  lnopcnre  31968  dmdbr2  32232  elatcv0  32270  iunsnima  32546  iunsnima2  32547  ecxpid  33332  ssdifidlprm  33429  ist0cld  33823  1stmbfm  34251  2ndmbfm  34252  eulerpartlemd  34357  oddprm2  34646  lfuhgr  35105  cvmlift2lem12  35301  bj-rest10  37076  topdifinfeq  37338  finxpsuclem  37385  curunc  37596  istotbnd2  37764  sstotbnd2  37768  isbnd3b  37779  totbndbnd  37783  br1cnvres  38258  fimgmcyc  42522  islnr2  43103  areaquad  43205  tfsconcat0i  43334  afv2res  47240  oddm1evenALTV  47676  oddp1evenALTV  47677  iscnrm3v  48941  isprsd  48943  joindm2  48956  meetdm2  48958  postcposALT  49557  postc  49558