Theorem baib 544

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  baibr  545  ceqsrexbv  3616  elrab3  3652  dfpss3  4044  rabsn  4688  elrint2  4956  opres  5990  cores  6252  fnres  6664  fvres  6902  fvmpti  6990  f1ompt  7108  fliftfun  7312  isocnv3  7332  riotaxfrd  7403  ovid  7553  nlimon  7848  limom  7879  brdifun  8726  elecreseq  8745  xpcomco  9056  0sdomg  9095  f1finf1o  9234  ordtypelem9  9489  isacn  10029  alephinit  10080  isfin5-2  10376  pwfseqlem1  10644  pwfseqlem3  10646  pwfseqlem4  10648  ltresr  11126  xrlenlt  11275  znnnlt1  12622  difrp  13057  elfz  13542  fzolb2  13697  elfzo3  13707  fzouzsplit  13725  rabssnn0fi  14024  caubnd  15412  ello12  15569  elo12  15580  bitsval2  16484  smueqlem  16549  rpexp  16782  ramcl  17090  ismon2  17792  isepi2  17799  isfull2  17971  isfth2  17975  ecxpid  19243  isghm3  19288  gastacos  19381  sylow2alem2  19689  lssnle  19745  isabl2  19861  submcmn2  19910  iscyggen2  19952  iscyg3  19957  cyggexb  19970  gsum2d2  20045  dprdw  20083  dprd2da  20115  iscrng2  20335  dvdsr2  20446  dfrhm2  20557  isdomn2  20797  sdrgacs  20885  islmhm3  21130  ssdifidlprm  21467  prmirredlem  21603  chrnzr  21661  iunocv  21812  iscss2  21817  ishil2  21850  obselocv  21859  psrbaglefi  22057  mplsubrglem  22134  bastop1  23131  isclo  23225  maxlp  23285  isperf2  23290  restperf  23322  cnpnei  23402  cnntr  23413  cnprest  23427  cnprest2  23428  lmres  23438  iscnrm2  23476  ist0-2  23482  ist1-2  23485  ishaus2  23489  tgcmp  23539  cmpfi  23546  dfconn2  23557  t1connperf  23574  subislly  23619  tx1cn  23747  tx2cn  23748  xkopt  23793  xkoinjcn  23825  ist0-4  23867  trfil2  24025  fin1aufil  24070  flimtopon  24108  elflim  24109  fclstopon  24150  isfcls2  24151  alexsubALTlem4  24188  ptcmplem3  24192  tgphaus  24255  xmetec  24572  prdsbl  24629  blval2  24700  isnvc2  24837  isnghm2  24862  isnmhm2  24890  0nmhm  24893  xrtgioo  24945  cncfcnvcn  25065  evth  25099  nmhmcn  25260  cmsss  25491  lssbn  25492  srabn  25500  ishl2  25510  ivthlem2  25592  0plef  25812  itg2monolem1  25890  itg2cnlem1  25901  itg2cnlem2  25902  ellimc2  26017  dvne0  26151  ellogdm  26782  dcubic  26989  atans2  27074  amgm  27133  ftalem3  27217  pclogsum  27357  dchrelbas3  27380  lgsabs1  27478  dchrvmaeq0  27646  rpvmasum2  27654  tgjustf  28720  clwwlkwwlksb  30383  ajval  31191  bnsscmcl  31198  axhcompl-zf  31328  seq1hcau  31517  hlim2  31522  issh3  31549  lnopcnre  32369  dmdbr2  32633  elatcv0  32671  iunsnima  32941  iunsnima2  32942  partfun2  32999  ist0cld  34201  1stmbfm  34628  2ndmbfm  34629  eulerpartlemd  34734  oddprm2  35020  scottrankeqel  35495  lfuhgr  35588  cvmlift2lem12  35784  bj-rest10  37708  topdifinfeq  37974  finxpsuclem  38021  curunc  38231  istotbnd2  38399  sstotbnd2  38403  isbnd3b  38414  totbndbnd  38418  br1cnvres  38901  fimgmcyc  43282  islnr2  43821  areaquad  43923  tfsconcat0i  44052  afv2res  47953  oddm1evenALTV  48417  oddp1evenALTV  48418  crngprmringdom  49084  iscnrm3v  49708  isprsd  49710  joindm2  49723  meetdm2  49725  postcposALT  50323  postc  50324