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  3607  elrab3  3644  dfpss3  4038  rabsn  4673  elrint2  4940  opres  5942  cores  6201  fnres  6613  fvres  6847  fvmpti  6934  f1ompt  7050  fliftfun  7252  isocnv3  7272  riotaxfrd  7343  ovid  7493  nlimon  7787  limom  7818  brdifun  8658  elecreseq  8677  xpcomco  8987  0sdomg  9026  f1finf1o  9164  ordtypelem9  9419  isacn  9942  alephinit  9993  isfin5-2  10289  pwfseqlem1  10556  pwfseqlem3  10558  pwfseqlem4  10560  ltresr  11038  xrlenlt  11184  znnnlt1  12505  difrp  12932  elfz  13415  fzolb2  13568  elfzo3  13578  fzouzsplit  13596  rabssnn0fi  13895  caubnd  15268  ello12  15425  elo12  15436  bitsval2  16338  smueqlem  16403  rpexp  16635  ramcl  16943  ismon2  17643  isepi2  17650  isfull2  17822  isfth2  17826  isghm3  19131  gastacos  19224  sylow2alem2  19532  lssnle  19588  isabl2  19704  submcmn2  19753  iscyggen2  19795  iscyg3  19800  cyggexb  19813  gsum2d2  19888  dprdw  19926  dprd2da  19958  iscrng2  20172  dvdsr2  20283  dfrhm2  20394  isdomn2  20628  isdomn2OLD  20629  sdrgacs  20718  islmhm3  20964  prmirredlem  21411  chrnzr  21469  iunocv  21620  iscss2  21625  ishil2  21658  obselocv  21667  psrbaglefi  21865  mplsubrglem  21942  bastop1  22909  isclo  23003  maxlp  23063  isperf2  23068  restperf  23100  cnpnei  23180  cnntr  23191  cnprest  23205  cnprest2  23206  lmres  23216  iscnrm2  23254  ist0-2  23260  ist1-2  23263  ishaus2  23267  tgcmp  23317  cmpfi  23324  dfconn2  23335  t1connperf  23352  subislly  23397  tx1cn  23525  tx2cn  23526  xkopt  23571  xkoinjcn  23603  ist0-4  23645  trfil2  23803  fin1aufil  23848  flimtopon  23886  elflim  23887  fclstopon  23928  isfcls2  23929  alexsubALTlem4  23966  ptcmplem3  23970  tgphaus  24033  xmetec  24350  prdsbl  24407  blval2  24478  isnvc2  24615  isnghm2  24640  isnmhm2  24668  0nmhm  24671  xrtgioo  24723  cncfcnvcn  24847  evth  24886  nmhmcn  25048  cmsss  25279  lssbn  25280  srabn  25288  ishl2  25298  ivthlem2  25381  0plef  25601  itg2monolem1  25679  itg2cnlem1  25690  itg2cnlem2  25691  ellimc2  25806  dvne0  25944  ellogdm  26576  dcubic  26784  atans2  26869  amgm  26929  ftalem3  27013  pclogsum  27154  dchrelbas3  27177  lgsabs1  27275  dchrvmaeq0  27443  rpvmasum2  27451  tgjustf  28452  clwwlkwwlksb  30036  ajval  30843  bnsscmcl  30850  axhcompl-zf  30980  seq1hcau  31169  hlim2  31174  issh3  31201  lnopcnre  32021  dmdbr2  32285  elatcv0  32323  iunsnima  32603  iunsnima2  32604  partfun2  32661  ecxpid  33333  ssdifidlprm  33430  ist0cld  33867  1stmbfm  34294  2ndmbfm  34295  eulerpartlemd  34400  oddprm2  34689  lfuhgr  35183  cvmlift2lem12  35379  bj-rest10  37153  topdifinfeq  37415  finxpsuclem  37462  curunc  37662  istotbnd2  37830  sstotbnd2  37834  isbnd3b  37845  totbndbnd  37849  br1cnvres  38326  fimgmcyc  42652  islnr2  43231  areaquad  43333  tfsconcat0i  43462  afv2res  47363  oddm1evenALTV  47799  oddp1evenALTV  47800  iscnrm3v  49077  isprsd  49079  joindm2  49092  meetdm2  49094  postcposALT  49693  postc  49694