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  3611  elrab3  3648  dfpss3  4039  rabsn  4674  elrint2  4940  opres  5938  cores  6196  fnres  6608  fvres  6841  fvmpti  6928  f1ompt  7044  fliftfun  7246  isocnv3  7266  riotaxfrd  7337  ovid  7487  nlimon  7781  limom  7812  brdifun  8652  elecreseq  8671  xpcomco  8980  0sdomg  9019  f1finf1o  9157  ordtypelem9  9412  isacn  9932  alephinit  9983  isfin5-2  10279  pwfseqlem1  10546  pwfseqlem3  10548  pwfseqlem4  10550  ltresr  11028  xrlenlt  11174  znnnlt1  12496  difrp  12927  elfz  13410  fzolb2  13563  elfzo3  13573  fzouzsplit  13591  rabssnn0fi  13890  caubnd  15263  ello12  15420  elo12  15431  bitsval2  16333  smueqlem  16398  rpexp  16630  ramcl  16938  ismon2  17638  isepi2  17645  isfull2  17817  isfth2  17821  isghm3  19127  gastacos  19220  sylow2alem2  19528  lssnle  19584  isabl2  19700  submcmn2  19749  iscyggen2  19791  iscyg3  19796  cyggexb  19809  gsum2d2  19884  dprdw  19922  dprd2da  19954  iscrng2  20168  dvdsr2  20279  dfrhm2  20390  isdomn2  20624  isdomn2OLD  20625  sdrgacs  20714  islmhm3  20960  prmirredlem  21407  chrnzr  21465  iunocv  21616  iscss2  21621  ishil2  21654  obselocv  21663  psrbaglefi  21861  mplsubrglem  21939  bastop1  22906  isclo  23000  maxlp  23060  isperf2  23065  restperf  23097  cnpnei  23177  cnntr  23188  cnprest  23202  cnprest2  23203  lmres  23213  iscnrm2  23251  ist0-2  23257  ist1-2  23260  ishaus2  23264  tgcmp  23314  cmpfi  23321  dfconn2  23332  t1connperf  23349  subislly  23394  tx1cn  23522  tx2cn  23523  xkopt  23568  xkoinjcn  23600  ist0-4  23642  trfil2  23800  fin1aufil  23845  flimtopon  23883  elflim  23884  fclstopon  23925  isfcls2  23926  alexsubALTlem4  23963  ptcmplem3  23967  tgphaus  24030  xmetec  24347  prdsbl  24404  blval2  24475  isnvc2  24612  isnghm2  24637  isnmhm2  24665  0nmhm  24668  xrtgioo  24720  cncfcnvcn  24844  evth  24883  nmhmcn  25045  cmsss  25276  lssbn  25277  srabn  25285  ishl2  25295  ivthlem2  25378  0plef  25598  itg2monolem1  25676  itg2cnlem1  25687  itg2cnlem2  25688  ellimc2  25803  dvne0  25941  ellogdm  26573  dcubic  26781  atans2  26866  amgm  26926  ftalem3  27010  pclogsum  27151  dchrelbas3  27174  lgsabs1  27272  dchrvmaeq0  27440  rpvmasum2  27448  tgjustf  28449  clwwlkwwlksb  30029  ajval  30836  bnsscmcl  30843  axhcompl-zf  30973  seq1hcau  31162  hlim2  31167  issh3  31194  lnopcnre  32014  dmdbr2  32278  elatcv0  32316  iunsnima  32596  iunsnima2  32597  ecxpid  33321  ssdifidlprm  33418  ist0cld  33841  1stmbfm  34268  2ndmbfm  34269  eulerpartlemd  34374  oddprm2  34663  lfuhgr  35150  cvmlift2lem12  35346  bj-rest10  37121  topdifinfeq  37383  finxpsuclem  37430  curunc  37641  istotbnd2  37809  sstotbnd2  37813  isbnd3b  37824  totbndbnd  37828  br1cnvres  38303  fimgmcyc  42566  islnr2  43146  areaquad  43248  tfsconcat0i  43377  afv2res  47269  oddm1evenALTV  47705  oddp1evenALTV  47706  iscnrm3v  48983  isprsd  48985  joindm2  48998  meetdm2  49000  postcposALT  49599  postc  49600