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  3609  elrab3  3645  dfpss3  4016  rabsn  4678  elrint2  4949  opres  5979  cores  6250  fnres  6666  fvres  6904  fvmpti  6992  f1ompt  7111  fliftfun  7320  isocnv3  7340  riotaxfrd  7411  ovid  7561  nlimon  7862  limom  7893  brdifun  8751  elecreseq  8770  xpcomco  9089  0sdomg  9128  f1finf1o  9267  ordtypelem9  9523  isacn  10126  alephinit  10177  isfin5-2  10472  pwfseqlem1  10746  pwfseqlem3  10748  pwfseqlem4  10750  ltresr  11228  xrlenlt  11377  znnnlt1  12726  difrp  13163  elfz  13648  fzolb2  13804  elfzo3  13814  fzouzsplit  13832  rabssnn0fi  14132  caubnd  15531  ello12  15688  elo12  15699  bitsval2  16600  smueqlem  16665  rpexp  16903  ramcl  17212  ismon2  17914  isepi2  17921  isfull2  18093  isfth2  18097  ecxpid  19391  isghm3  19436  gastacos  19529  sylow2alem2  19837  lssnle  19893  isabl2  20009  submcmn2  20058  iscyggen2  20100  iscyg3  20105  cyggexb  20118  gsum2d2  20193  dprdw  20231  dprd2da  20263  iscrng2  20484  dvdsr2  20598  dfrhm2  20709  brric2  20759  isdomn2  20968  sdrgacs  21063  islmhm3  21308  ssdifidlprm  21647  prmirredlem  21783  chrnzr  21841  iunocv  21992  iscss2  21997  ishil2  22030  obselocv  22039  psrbaglefi  22239  mplsubrglem  22316  bastop1  23316  isclo  23410  maxlp  23470  isperf2  23475  restperf  23507  cnpnei  23587  cnntr  23598  cnprest  23612  cnprest2  23613  lmres  23623  iscnrm2  23661  ist0-2  23667  ist1-2  23670  ishaus2  23674  tgcmp  23724  cmpfi  23731  dfconn2  23742  t1connperf  23759  subislly  23805  tx1cn  23933  tx2cn  23934  xkopt  23979  xkoinjcn  24011  ist0-4  24053  trfil2  24211  fin1aufil  24256  flimtopon  24294  elflim  24295  fclstopon  24336  isfcls2  24337  alexsubALTlem4  24374  ptcmplem3  24378  tgphaus  24441  xmetec  24758  prdsbl  24815  blval2  24886  isnvc2  25023  isnghm2  25048  isnmhm2  25076  0nmhm  25079  xrtgioo  25131  cncfcnvcn  25251  evth  25285  nmhmcn  25446  cmsss  25677  lssbn  25678  srabn  25686  ishl2  25696  ivthlem2  25778  0plef  25998  itg2monolem1  26076  itg2cnlem1  26087  itg2cnlem2  26088  ellimc2  26202  dvne0  26336  ellogdm  26972  dcubic  27179  atans2  27264  amgm  27323  ftalem3  27407  pclogsum  27547  dchrelbas3  27570  lgsabs1  27668  dchrvmaeq0  27836  rpvmasum2  27844  tgjustf  28940  lfuhgr  29731  clwwlkwwlksb  30650  ajval  31468  bnsscmcl  31475  axhcompl-zf  31605  seq1hcau  31794  hlim2  31799  issh3  31826  lnopcnre  32646  dmdbr2  32910  elatcv0  32948  iunsnima  33259  iunsnima2  33260  partfun2  33317  ist0cld  34511  1stmbfm  34938  2ndmbfm  34939  eulerpartlemd  35044  oddprm2  35330  fwfffunres  35764  scottrankeqel  35802  cvmlift2lem12  36165  bj-rest10  38101  topdifinfeq  38366  finxpsuclem  38413  curunc  38618  istotbnd2  38797  sstotbnd2  38801  isbnd3b  38812  totbndbnd  38816  br1cnvres  39299  fimgmcyc  43691  islnr2  44209  areaquad  44311  tfsconcat0i  44440  afv2res  48402  oddm1evenALTV  48866  oddp1evenALTV  48867  crngprmringdom  49532  iscnrm3v  50160  isprsd  50162  joindm2  50175  meetdm2  50177  postcposALT  50799  postc  50800  dvsec  51024  dvcsc  51025  dvcot  51026