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  3599  elrab3  3636  dfpss3  4030  rabsn  4666  elrint2  4933  opres  5948  cores  6207  fnres  6619  fvres  6853  fvmpti  6940  f1ompt  7057  fliftfun  7260  isocnv3  7280  riotaxfrd  7351  ovid  7501  nlimon  7795  limom  7826  brdifun  8667  elecreseq  8686  xpcomco  8998  0sdomg  9037  f1finf1o  9176  ordtypelem9  9434  isacn  9957  alephinit  10008  isfin5-2  10304  pwfseqlem1  10572  pwfseqlem3  10574  pwfseqlem4  10576  ltresr  11054  xrlenlt  11201  znnnlt1  12545  difrp  12973  elfz  13458  fzolb2  13612  elfzo3  13622  fzouzsplit  13640  rabssnn0fi  13939  caubnd  15312  ello12  15469  elo12  15480  bitsval2  16385  smueqlem  16450  rpexp  16683  ramcl  16991  ismon2  17692  isepi2  17699  isfull2  17871  isfth2  17875  isghm3  19183  gastacos  19276  sylow2alem2  19584  lssnle  19640  isabl2  19756  submcmn2  19805  iscyggen2  19847  iscyg3  19852  cyggexb  19865  gsum2d2  19940  dprdw  19978  dprd2da  20010  iscrng2  20224  dvdsr2  20334  dfrhm2  20445  isdomn2  20679  isdomn2OLD  20680  sdrgacs  20769  islmhm3  21015  prmirredlem  21462  chrnzr  21520  iunocv  21671  iscss2  21676  ishil2  21709  obselocv  21718  psrbaglefi  21916  mplsubrglem  21992  bastop1  22968  isclo  23062  maxlp  23122  isperf2  23127  restperf  23159  cnpnei  23239  cnntr  23250  cnprest  23264  cnprest2  23265  lmres  23275  iscnrm2  23313  ist0-2  23319  ist1-2  23322  ishaus2  23326  tgcmp  23376  cmpfi  23383  dfconn2  23394  t1connperf  23411  subislly  23456  tx1cn  23584  tx2cn  23585  xkopt  23630  xkoinjcn  23662  ist0-4  23704  trfil2  23862  fin1aufil  23907  flimtopon  23945  elflim  23946  fclstopon  23987  isfcls2  23988  alexsubALTlem4  24025  ptcmplem3  24029  tgphaus  24092  xmetec  24409  prdsbl  24466  blval2  24537  isnvc2  24674  isnghm2  24699  isnmhm2  24727  0nmhm  24730  xrtgioo  24782  cncfcnvcn  24902  evth  24936  nmhmcn  25097  cmsss  25328  lssbn  25329  srabn  25337  ishl2  25347  ivthlem2  25429  0plef  25649  itg2monolem1  25727  itg2cnlem1  25738  itg2cnlem2  25739  ellimc2  25854  dvne0  25988  ellogdm  26616  dcubic  26823  atans2  26908  amgm  26968  ftalem3  27052  pclogsum  27192  dchrelbas3  27215  lgsabs1  27313  dchrvmaeq0  27481  rpvmasum2  27489  tgjustf  28555  clwwlkwwlksb  30139  ajval  30947  bnsscmcl  30954  axhcompl-zf  31084  seq1hcau  31273  hlim2  31278  issh3  31305  lnopcnre  32125  dmdbr2  32389  elatcv0  32427  iunsnima  32706  iunsnima2  32707  partfun2  32764  ecxpid  33436  ssdifidlprm  33533  ist0cld  33993  1stmbfm  34420  2ndmbfm  34421  eulerpartlemd  34526  oddprm2  34815  lfuhgr  35316  cvmlift2lem12  35512  bj-rest10  37416  topdifinfeq  37680  finxpsuclem  37727  curunc  37937  istotbnd2  38105  sstotbnd2  38109  isbnd3b  38120  totbndbnd  38124  br1cnvres  38609  fimgmcyc  42993  islnr2  43560  areaquad  43662  tfsconcat0i  43791  afv2res  47699  oddm1evenALTV  48163  oddp1evenALTV  48164  iscnrm3v  49440  isprsd  49442  joindm2  49455  meetdm2  49457  postcposALT  50055  postc  50056