Theorem baib 538

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		ibar 531	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
2		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	1, 2	syl6rbbr 292	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  baibr  539  ceqsrexbv  3653  elrab3  3684  dfpss3  4066  rabsn  4660  elrint2  4921  opres  5866  cores  6105  elpredg  6165  fnres  6477  fvres  6692  fvmpti  6770  f1ompt  6878  fliftfun  7068  isocnv3  7088  riotaxfrd  7151  ovid  7294  nlimon  7569  limom  7598  brdifun  8321  xpcomco  8610  0sdomg  8649  f1finf1o  8748  ordtypelem9  8993  isacn  9473  alephinit  9524  isfin5-2  9816  pwfseqlem1  10083  pwfseqlem3  10085  pwfseqlem4  10087  ltresr  10565  xrlenlt  10709  znnnlt1  12012  difrp  12430  elfz  12901  fzolb2  13048  elfzo3  13057  fzouzsplit  13075  rabssnn0fi  13357  caubnd  14721  ello12  14876  elo12  14887  bitsval2  15777  smueqlem  15842  rpexp  16067  ramcl  16368  ismon2  17007  isepi2  17014  isfull2  17184  isfth2  17188  isghm3  18362  gastacos  18443  sylow2alem2  18746  lssnle  18803  isabl2  18918  submcmn2  18962  iscyggen2  19003  iscyg3  19008  cyggexb  19022  gsum2d2  19097  dprdw  19135  dprd2da  19167  iscrng2  19316  dvdsr2  19400  dfrhm2  19472  sdrgacs  19583  islmhm3  19803  isdomn2  20075  psrbaglefi  20155  mplsubrglem  20222  prmirredlem  20643  chrnzr  20680  iunocv  20828  iscss2  20833  ishil2  20866  obselocv  20875  bastop1  21604  isclo  21698  maxlp  21758  isperf2  21763  restperf  21795  cnpnei  21875  cnntr  21886  cnprest  21900  cnprest2  21901  lmres  21911  iscnrm2  21949  ist0-2  21955  ist1-2  21958  ishaus2  21962  tgcmp  22012  cmpfi  22019  dfconn2  22030  t1connperf  22047  subislly  22092  tx1cn  22220  tx2cn  22221  xkopt  22266  xkoinjcn  22298  ist0-4  22340  trfil2  22498  fin1aufil  22543  flimtopon  22581  elflim  22582  fclstopon  22623  isfcls2  22624  alexsubALTlem4  22661  ptcmplem3  22665  tgphaus  22728  xmetec  23047  prdsbl  23104  blval2  23175  isnvc2  23311  isnghm2  23336  isnmhm2  23364  0nmhm  23367  xrtgioo  23417  cncfcnvcn  23532  evth  23566  nmhmcn  23727  cmsss  23957  lssbn  23958  srabn  23966  ishl2  23976  ivthlem2  24056  0plef  24276  itg2monolem1  24354  itg2cnlem1  24365  itg2cnlem2  24366  ellimc2  24478  dvne0  24611  ellogdm  25225  dcubic  25427  atans2  25512  amgm  25571  ftalem3  25655  pclogsum  25794  dchrelbas3  25817  lgsabs1  25915  dchrvmaeq0  26083  rpvmasum2  26091  tgjustf  26262  clwwlkwwlksb  27836  ajval  28641  bnsscmcl  28648  axhcompl-zf  28778  seq1hcau  28967  hlim2  28972  issh3  28999  lnopcnre  29819  dmdbr2  30083  elatcv0  30121  iunsnima  30372  ecxpid  30929  1stmbfm  31522  2ndmbfm  31523  eulerpartlemd  31628  oddprm2  31930  lfuhgr  32368  cvmlift2lem12  32565  bj-rest10  34383  topdifinfeq  34635  finxpsuclem  34682  curunc  34878  istotbnd2  35052  sstotbnd2  35056  isbnd3b  35067  totbndbnd  35071  ecres2  35540  islnr2  39720  areaquad  39829  afv2res  43445  oddm1evenALTV  43847  oddp1evenALTV  43848