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  3613  elrab3  3649  dfpss3  4040  rabsn  4685  elrint2  4953  opres  5986  cores  6249  fnres  6663  fvres  6901  fvmpti  6989  f1ompt  7108  fliftfun  7317  isocnv3  7337  riotaxfrd  7408  ovid  7558  nlimon  7851  limom  7882  brdifun  8731  elecreseq  8750  xpcomco  9069  0sdomg  9108  f1finf1o  9247  ordtypelem9  9502  isacn  10051  alephinit  10102  isfin5-2  10397  pwfseqlem1  10671  pwfseqlem3  10673  pwfseqlem4  10675  ltresr  11153  xrlenlt  11302  znnnlt1  12649  difrp  13086  elfz  13571  fzolb2  13726  elfzo3  13736  fzouzsplit  13754  rabssnn0fi  14054  caubnd  15450  ello12  15607  elo12  15618  bitsval2  16521  smueqlem  16586  rpexp  16819  ramcl  17127  ismon2  17829  isepi2  17836  isfull2  18008  isfth2  18012  ecxpid  19305  isghm3  19350  gastacos  19443  sylow2alem2  19751  lssnle  19807  isabl2  19923  submcmn2  19972  iscyggen2  20014  iscyg3  20019  cyggexb  20032  gsum2d2  20107  dprdw  20145  dprd2da  20177  iscrng2  20397  dvdsr2  20510  dfrhm2  20621  brric2  20671  isdomn2  20879  sdrgacs  20973  islmhm3  21218  ssdifidlprm  21555  prmirredlem  21691  chrnzr  21749  iunocv  21900  iscss2  21905  ishil2  21938  obselocv  21947  psrbaglefi  22147  mplsubrglem  22224  bastop1  23224  isclo  23318  maxlp  23378  isperf2  23383  restperf  23415  cnpnei  23495  cnntr  23506  cnprest  23520  cnprest2  23521  lmres  23531  iscnrm2  23569  ist0-2  23575  ist1-2  23578  ishaus2  23582  tgcmp  23632  cmpfi  23639  dfconn2  23650  t1connperf  23667  subislly  23713  tx1cn  23841  tx2cn  23842  xkopt  23887  xkoinjcn  23919  ist0-4  23961  trfil2  24119  fin1aufil  24164  flimtopon  24202  elflim  24203  fclstopon  24244  isfcls2  24245  alexsubALTlem4  24282  ptcmplem3  24286  tgphaus  24349  xmetec  24666  prdsbl  24723  blval2  24794  isnvc2  24931  isnghm2  24956  isnmhm2  24984  0nmhm  24987  xrtgioo  25039  cncfcnvcn  25159  evth  25193  nmhmcn  25354  cmsss  25585  lssbn  25586  srabn  25594  ishl2  25604  ivthlem2  25686  0plef  25906  itg2monolem1  25984  itg2cnlem1  25995  itg2cnlem2  25996  ellimc2  26111  dvne0  26245  ellogdm  26884  dcubic  27091  atans2  27176  amgm  27235  ftalem3  27319  pclogsum  27459  dchrelbas3  27482  lgsabs1  27580  dchrvmaeq0  27748  rpvmasum2  27756  tgjustf  28822  lfuhgr  29613  clwwlkwwlksb  30532  ajval  31350  bnsscmcl  31357  axhcompl-zf  31487  seq1hcau  31676  hlim2  31681  issh3  31708  lnopcnre  32528  dmdbr2  32792  elatcv0  32830  iunsnima  33099  iunsnima2  33100  partfun2  33157  ist0cld  34351  1stmbfm  34779  2ndmbfm  34780  eulerpartlemd  34885  oddprm2  35171  scottrankeqel  35639  cvmlift2lem12  35901  bj-rest10  37846  topdifinfeq  38112  finxpsuclem  38159  curunc  38364  istotbnd2  38528  sstotbnd2  38532  isbnd3b  38543  totbndbnd  38547  br1cnvres  39030  fimgmcyc  43424  islnr2  43963  areaquad  44065  tfsconcat0i  44194  afv2res  48135  oddm1evenALTV  48599  oddp1evenALTV  48600  crngprmringdom  49265  iscnrm3v  49887  isprsd  49889  joindm2  49902  meetdm2  49904  postcposALT  50502  postc  50503  dvsec  50697  dvcsc  50698  dvcot  50699