Theorem baib 545

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 538	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	bitr4id 293	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  baibr  546  ceqsrexbv  3618  elrab3  3654  dfpss3  4046  rabsn  4692  elrint2  4960  opres  5993  cores  6255  fnres  6669  fvres  6907  fvmpti  6995  f1ompt  7113  fliftfun  7321  isocnv3  7341  riotaxfrd  7414  ovid  7564  nlimon  7856  limom  7887  brdifun  8734  elecreseq  8753  xpcomco  9065  0sdomg  9104  f1finf1o  9243  ordtypelem9  9498  isacn  10047  alephinit  10098  isfin5-2  10393  pwfseqlem1  10661  pwfseqlem3  10663  pwfseqlem4  10665  ltresr  11143  xrlenlt  11292  znnnlt1  12639  difrp  13074  elfz  13559  fzolb2  13714  elfzo3  13724  fzouzsplit  13742  rabssnn0fi  14042  caubnd  15436  ello12  15593  elo12  15604  bitsval2  16508  smueqlem  16573  rpexp  16806  ramcl  17114  ismon2  17816  isepi2  17823  isfull2  17995  isfth2  17999  ecxpid  19273  isghm3  19318  gastacos  19411  sylow2alem2  19719  lssnle  19775  isabl2  19891  submcmn2  19940  iscyggen2  19982  iscyg3  19987  cyggexb  20000  gsum2d2  20075  dprdw  20113  dprd2da  20145  iscrng2  20365  dvdsr2  20478  dfrhm2  20589  brric2  20639  isdomn2  20847  sdrgacs  20941  islmhm3  21186  ssdifidlprm  21523  prmirredlem  21659  chrnzr  21717  iunocv  21868  iscss2  21873  ishil2  21906  obselocv  21915  psrbaglefi  22113  mplsubrglem  22190  bastop1  23187  isclo  23281  maxlp  23341  isperf2  23346  restperf  23378  cnpnei  23458  cnntr  23469  cnprest  23483  cnprest2  23484  lmres  23494  iscnrm2  23532  ist0-2  23538  ist1-2  23541  ishaus2  23545  tgcmp  23595  cmpfi  23602  dfconn2  23613  t1connperf  23630  subislly  23675  tx1cn  23803  tx2cn  23804  xkopt  23849  xkoinjcn  23881  ist0-4  23923  trfil2  24081  fin1aufil  24126  flimtopon  24164  elflim  24165  fclstopon  24206  isfcls2  24207  alexsubALTlem4  24244  ptcmplem3  24248  tgphaus  24311  xmetec  24628  prdsbl  24685  blval2  24756  isnvc2  24893  isnghm2  24918  isnmhm2  24946  0nmhm  24949  xrtgioo  25001  cncfcnvcn  25121  evth  25155  nmhmcn  25316  cmsss  25547  lssbn  25548  srabn  25556  ishl2  25566  ivthlem2  25648  0plef  25868  itg2monolem1  25946  itg2cnlem1  25957  itg2cnlem2  25958  ellimc2  26073  dvne0  26207  ellogdm  26841  dcubic  27048  atans2  27133  amgm  27192  ftalem3  27276  pclogsum  27416  dchrelbas3  27439  lgsabs1  27537  dchrvmaeq0  27705  rpvmasum2  27713  tgjustf  28779  clwwlkwwlksb  30442  ajval  31250  bnsscmcl  31257  axhcompl-zf  31387  seq1hcau  31576  hlim2  31581  issh3  31608  lnopcnre  32428  dmdbr2  32692  elatcv0  32730  iunsnima  33000  iunsnima2  33001  partfun2  33058  ist0cld  34254  1stmbfm  34682  2ndmbfm  34683  eulerpartlemd  34788  oddprm2  35074  scottrankeqel  35542  lfuhgr  35631  cvmlift2lem12  35827  bj-rest10  37771  topdifinfeq  38037  finxpsuclem  38084  curunc  38294  istotbnd2  38462  sstotbnd2  38466  isbnd3b  38477  totbndbnd  38481  br1cnvres  38964  fimgmcyc  43343  islnr2  43882  areaquad  43984  tfsconcat0i  44113  afv2res  48017  oddm1evenALTV  48481  oddp1evenALTV  48482  crngprmringdom  49148  iscnrm3v  49772  isprsd  49774  joindm2  49787  meetdm2  49789  postcposALT  50387  postc  50388