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  3598  elrab3  3635  dfpss3  4029  rabsn  4665  elrint2  4932  opres  5954  cores  6213  fnres  6625  fvres  6859  fvmpti  6946  f1ompt  7063  fliftfun  7267  isocnv3  7287  riotaxfrd  7358  ovid  7508  nlimon  7802  limom  7833  brdifun  8674  elecreseq  8693  xpcomco  9005  0sdomg  9044  f1finf1o  9183  ordtypelem9  9441  isacn  9966  alephinit  10017  isfin5-2  10313  pwfseqlem1  10581  pwfseqlem3  10583  pwfseqlem4  10585  ltresr  11063  xrlenlt  11210  znnnlt1  12554  difrp  12982  elfz  13467  fzolb2  13621  elfzo3  13631  fzouzsplit  13649  rabssnn0fi  13948  caubnd  15321  ello12  15478  elo12  15489  bitsval2  16394  smueqlem  16459  rpexp  16692  ramcl  17000  ismon2  17701  isepi2  17708  isfull2  17880  isfth2  17884  isghm3  19192  gastacos  19285  sylow2alem2  19593  lssnle  19649  isabl2  19765  submcmn2  19814  iscyggen2  19856  iscyg3  19861  cyggexb  19874  gsum2d2  19949  dprdw  19987  dprd2da  20019  iscrng2  20233  dvdsr2  20343  dfrhm2  20454  isdomn2  20688  isdomn2OLD  20689  sdrgacs  20778  islmhm3  21023  prmirredlem  21452  chrnzr  21510  iunocv  21661  iscss2  21666  ishil2  21699  obselocv  21708  psrbaglefi  21906  mplsubrglem  21982  bastop1  22958  isclo  23052  maxlp  23112  isperf2  23117  restperf  23149  cnpnei  23229  cnntr  23240  cnprest  23254  cnprest2  23255  lmres  23265  iscnrm2  23303  ist0-2  23309  ist1-2  23312  ishaus2  23316  tgcmp  23366  cmpfi  23373  dfconn2  23384  t1connperf  23401  subislly  23446  tx1cn  23574  tx2cn  23575  xkopt  23620  xkoinjcn  23652  ist0-4  23694  trfil2  23852  fin1aufil  23897  flimtopon  23935  elflim  23936  fclstopon  23977  isfcls2  23978  alexsubALTlem4  24015  ptcmplem3  24019  tgphaus  24082  xmetec  24399  prdsbl  24456  blval2  24527  isnvc2  24664  isnghm2  24689  isnmhm2  24717  0nmhm  24720  xrtgioo  24772  cncfcnvcn  24892  evth  24926  nmhmcn  25087  cmsss  25318  lssbn  25319  srabn  25327  ishl2  25337  ivthlem2  25419  0plef  25639  itg2monolem1  25717  itg2cnlem1  25728  itg2cnlem2  25729  ellimc2  25844  dvne0  25978  ellogdm  26603  dcubic  26810  atans2  26895  amgm  26954  ftalem3  27038  pclogsum  27178  dchrelbas3  27201  lgsabs1  27299  dchrvmaeq0  27467  rpvmasum2  27475  tgjustf  28541  clwwlkwwlksb  30124  ajval  30932  bnsscmcl  30939  axhcompl-zf  31069  seq1hcau  31258  hlim2  31263  issh3  31290  lnopcnre  32110  dmdbr2  32374  elatcv0  32412  iunsnima  32691  iunsnima2  32692  partfun2  32749  ecxpid  33421  ssdifidlprm  33518  ist0cld  33977  1stmbfm  34404  2ndmbfm  34405  eulerpartlemd  34510  oddprm2  34799  lfuhgr  35300  cvmlift2lem12  35496  bj-rest10  37400  topdifinfeq  37666  finxpsuclem  37713  curunc  37923  istotbnd2  38091  sstotbnd2  38095  isbnd3b  38106  totbndbnd  38110  br1cnvres  38595  fimgmcyc  42979  islnr2  43542  areaquad  43644  tfsconcat0i  43773  afv2res  47687  oddm1evenALTV  48151  oddp1evenALTV  48152  iscnrm3v  49428  isprsd  49430  joindm2  49443  meetdm2  49445  postcposALT  50043  postc  50044