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  3610  elrab3  3647  dfpss3  4041  rabsn  4678  elrint2  4945  opres  5948  cores  6207  fnres  6619  fvres  6853  fvmpti  6940  f1ompt  7056  fliftfun  7258  isocnv3  7278  riotaxfrd  7349  ovid  7499  nlimon  7793  limom  7824  brdifun  8665  elecreseq  8684  xpcomco  8995  0sdomg  9034  f1finf1o  9173  ordtypelem9  9431  isacn  9954  alephinit  10005  isfin5-2  10301  pwfseqlem1  10569  pwfseqlem3  10571  pwfseqlem4  10573  ltresr  11051  xrlenlt  11197  znnnlt1  12518  difrp  12945  elfz  13429  fzolb2  13582  elfzo3  13592  fzouzsplit  13610  rabssnn0fi  13909  caubnd  15282  ello12  15439  elo12  15450  bitsval2  16352  smueqlem  16417  rpexp  16649  ramcl  16957  ismon2  17658  isepi2  17665  isfull2  17837  isfth2  17841  isghm3  19146  gastacos  19239  sylow2alem2  19547  lssnle  19603  isabl2  19719  submcmn2  19768  iscyggen2  19810  iscyg3  19815  cyggexb  19828  gsum2d2  19903  dprdw  19941  dprd2da  19973  iscrng2  20187  dvdsr2  20299  dfrhm2  20410  isdomn2  20644  isdomn2OLD  20645  sdrgacs  20734  islmhm3  20980  prmirredlem  21427  chrnzr  21485  iunocv  21636  iscss2  21641  ishil2  21674  obselocv  21683  psrbaglefi  21882  mplsubrglem  21959  bastop1  22937  isclo  23031  maxlp  23091  isperf2  23096  restperf  23128  cnpnei  23208  cnntr  23219  cnprest  23233  cnprest2  23234  lmres  23244  iscnrm2  23282  ist0-2  23288  ist1-2  23291  ishaus2  23295  tgcmp  23345  cmpfi  23352  dfconn2  23363  t1connperf  23380  subislly  23425  tx1cn  23553  tx2cn  23554  xkopt  23599  xkoinjcn  23631  ist0-4  23673  trfil2  23831  fin1aufil  23876  flimtopon  23914  elflim  23915  fclstopon  23956  isfcls2  23957  alexsubALTlem4  23994  ptcmplem3  23998  tgphaus  24061  xmetec  24378  prdsbl  24435  blval2  24506  isnvc2  24643  isnghm2  24668  isnmhm2  24696  0nmhm  24699  xrtgioo  24751  cncfcnvcn  24875  evth  24914  nmhmcn  25076  cmsss  25307  lssbn  25308  srabn  25316  ishl2  25326  ivthlem2  25409  0plef  25629  itg2monolem1  25707  itg2cnlem1  25718  itg2cnlem2  25719  ellimc2  25834  dvne0  25972  ellogdm  26604  dcubic  26812  atans2  26897  amgm  26957  ftalem3  27041  pclogsum  27182  dchrelbas3  27205  lgsabs1  27303  dchrvmaeq0  27471  rpvmasum2  27479  tgjustf  28545  clwwlkwwlksb  30129  ajval  30936  bnsscmcl  30943  axhcompl-zf  31073  seq1hcau  31262  hlim2  31267  issh3  31294  lnopcnre  32114  dmdbr2  32378  elatcv0  32416  iunsnima  32696  iunsnima2  32697  partfun2  32755  ecxpid  33442  ssdifidlprm  33539  ist0cld  33990  1stmbfm  34417  2ndmbfm  34418  eulerpartlemd  34523  oddprm2  34812  lfuhgr  35312  cvmlift2lem12  35508  bj-rest10  37289  topdifinfeq  37551  finxpsuclem  37598  curunc  37799  istotbnd2  37967  sstotbnd2  37971  isbnd3b  37982  totbndbnd  37986  br1cnvres  38463  fimgmcyc  42785  islnr2  43352  areaquad  43454  tfsconcat0i  43583  afv2res  47481  oddm1evenALTV  47917  oddp1evenALTV  47918  iscnrm3v  49194  isprsd  49196  joindm2  49209  meetdm2  49211  postcposALT  49809  postc  49810