Theorem baib 537

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  baibr  538  ceqsrexbv  3643  elrab3  3683  dfpss3  4085  rabsn  4724  elrint2  4995  opres  5989  cores  6245  fnres  6674  fvres  6907  fvmpti  6993  f1ompt  7106  fliftfun  7304  isocnv3  7324  riotaxfrd  7395  ovid  7544  nlimon  7835  limom  7866  brdifun  8728  xpcomco  9058  0sdomg  9100  0sdomgOLD  9101  f1finf1o  9267  f1finf1oOLD  9268  ordtypelem9  9517  isacn  10035  alephinit  10086  isfin5-2  10382  pwfseqlem1  10649  pwfseqlem3  10651  pwfseqlem4  10653  ltresr  11131  xrlenlt  11275  znnnlt1  12585  difrp  13008  elfz  13486  fzolb2  13635  elfzo3  13645  fzouzsplit  13663  rabssnn0fi  13947  caubnd  15301  ello12  15456  elo12  15467  bitsval2  16362  smueqlem  16427  rpexp  16655  ramcl  16958  ismon2  17677  isepi2  17684  isfull2  17858  isfth2  17862  isghm3  19087  gastacos  19168  sylow2alem2  19479  lssnle  19535  isabl2  19651  submcmn2  19699  iscyggen2  19741  iscyg3  19746  cyggexb  19759  gsum2d2  19834  dprdw  19872  dprd2da  19904  iscrng2  20066  dvdsr2  20166  dfrhm2  20242  sdrgacs  20405  islmhm3  20627  isdomn2  20902  prmirredlem  21026  chrnzr  21066  iunocv  21218  iscss2  21223  ishil2  21258  obselocv  21267  psrbaglefi  21467  psrbaglefiOLD  21468  mplsubrglem  21545  bastop1  22478  isclo  22573  maxlp  22633  isperf2  22638  restperf  22670  cnpnei  22750  cnntr  22761  cnprest  22775  cnprest2  22776  lmres  22786  iscnrm2  22824  ist0-2  22830  ist1-2  22833  ishaus2  22837  tgcmp  22887  cmpfi  22894  dfconn2  22905  t1connperf  22922  subislly  22967  tx1cn  23095  tx2cn  23096  xkopt  23141  xkoinjcn  23173  ist0-4  23215  trfil2  23373  fin1aufil  23418  flimtopon  23456  elflim  23457  fclstopon  23498  isfcls2  23499  alexsubALTlem4  23536  ptcmplem3  23540  tgphaus  23603  xmetec  23922  prdsbl  23982  blval2  24053  isnvc2  24198  isnghm2  24223  isnmhm2  24251  0nmhm  24254  xrtgioo  24304  cncfcnvcn  24423  evth  24457  nmhmcn  24618  cmsss  24850  lssbn  24851  srabn  24859  ishl2  24869  ivthlem2  24951  0plef  25171  itg2monolem1  25250  itg2cnlem1  25261  itg2cnlem2  25262  ellimc2  25376  dvne0  25510  ellogdm  26129  dcubic  26331  atans2  26416  amgm  26475  ftalem3  26559  pclogsum  26698  dchrelbas3  26721  lgsabs1  26819  dchrvmaeq0  26987  rpvmasum2  26995  tgjustf  27704  clwwlkwwlksb  29287  ajval  30092  bnsscmcl  30099  axhcompl-zf  30229  seq1hcau  30418  hlim2  30423  issh3  30450  lnopcnre  31270  dmdbr2  31534  elatcv0  31572  iunsnima  31825  iunsnima2  31826  ecxpid  32441  ist0cld  32751  1stmbfm  33197  2ndmbfm  33198  eulerpartlemd  33303  oddprm2  33605  lfuhgr  34046  cvmlift2lem12  34243  bj-rest10  35907  topdifinfeq  36169  finxpsuclem  36216  curunc  36408  istotbnd2  36576  sstotbnd2  36580  isbnd3b  36591  totbndbnd  36595  br1cnvres  37075  ecres2  37085  islnr2  41789  areaquad  41898  tfsconcat0i  42028  afv2res  45882  oddm1evenALTV  46278  oddp1evenALTV  46279  iscnrm3v  47488  isprsd  47490  joindm2  47503  meetdm2  47505  postcposALT  47603  postc  47604