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  19267  isghm3  19312  gastacos  19405  sylow2alem2  19713  lssnle  19769  isabl2  19885  submcmn2  19934  iscyggen2  19976  iscyg3  19981  cyggexb  19994  gsum2d2  20069  dprdw  20107  dprd2da  20139  iscrng2  20359  dvdsr2  20471  dfrhm2  20582  brric2  20632  isdomn2  20840  sdrgacs  20934  islmhm3  21179  ssdifidlprm  21516  prmirredlem  21652  chrnzr  21710  iunocv  21861  iscss2  21866  ishil2  21899  obselocv  21908  psrbaglefi  22106  mplsubrglem  22183  bastop1  23180  isclo  23274  maxlp  23334  isperf2  23339  restperf  23371  cnpnei  23451  cnntr  23462  cnprest  23476  cnprest2  23477  lmres  23487  iscnrm2  23525  ist0-2  23531  ist1-2  23534  ishaus2  23538  tgcmp  23588  cmpfi  23595  dfconn2  23606  t1connperf  23623  subislly  23668  tx1cn  23796  tx2cn  23797  xkopt  23842  xkoinjcn  23874  ist0-4  23916  trfil2  24074  fin1aufil  24119  flimtopon  24157  elflim  24158  fclstopon  24199  isfcls2  24200  alexsubALTlem4  24237  ptcmplem3  24241  tgphaus  24304  xmetec  24621  prdsbl  24678  blval2  24749  isnvc2  24886  isnghm2  24911  isnmhm2  24939  0nmhm  24942  xrtgioo  24994  cncfcnvcn  25114  evth  25148  nmhmcn  25309  cmsss  25540  lssbn  25541  srabn  25549  ishl2  25559  ivthlem2  25641  0plef  25861  itg2monolem1  25939  itg2cnlem1  25950  itg2cnlem2  25951  ellimc2  26066  dvne0  26200  ellogdm  26834  dcubic  27041  atans2  27126  amgm  27185  ftalem3  27269  pclogsum  27409  dchrelbas3  27432  lgsabs1  27530  dchrvmaeq0  27698  rpvmasum2  27706  tgjustf  28772  clwwlkwwlksb  30435  ajval  31243  bnsscmcl  31250  axhcompl-zf  31380  seq1hcau  31569  hlim2  31574  issh3  31601  lnopcnre  32421  dmdbr2  32685  elatcv0  32723  iunsnima  32993  iunsnima2  32994  partfun2  33051  ist0cld  34247  1stmbfm  34674  2ndmbfm  34675  eulerpartlemd  34780  oddprm2  35066  scottrankeqel  35534  lfuhgr  35623  cvmlift2lem12  35819  bj-rest10  37763  topdifinfeq  38029  finxpsuclem  38076  curunc  38286  istotbnd2  38454  sstotbnd2  38458  isbnd3b  38469  totbndbnd  38473  br1cnvres  38956  fimgmcyc  43335  islnr2  43874  areaquad  43976  tfsconcat0i  44105  afv2res  48009  oddm1evenALTV  48473  oddp1evenALTV  48474  crngprmringdom  49140  iscnrm3v  49764  isprsd  49766  joindm2  49779  meetdm2  49781  postcposALT  50379  postc  50380