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  3610  elrab3  3646  dfpss3  4037  rabsn  4682  elrint2  4950  opres  5980  cores  6243  fnres  6658  fvres  6896  fvmpti  6984  f1ompt  7103  fliftfun  7312  isocnv3  7332  riotaxfrd  7403  ovid  7553  nlimon  7851  limom  7882  brdifun  8732  elecreseq  8751  xpcomco  9070  0sdomg  9109  f1finf1o  9248  ordtypelem9  9504  isacn  10104  alephinit  10155  isfin5-2  10450  pwfseqlem1  10724  pwfseqlem3  10726  pwfseqlem4  10728  ltresr  11206  xrlenlt  11355  znnnlt1  12704  difrp  13141  elfz  13626  fzolb2  13781  elfzo3  13791  fzouzsplit  13809  rabssnn0fi  14109  caubnd  15506  ello12  15663  elo12  15674  bitsval2  16575  smueqlem  16640  rpexp  16878  ramcl  17187  ismon2  17889  isepi2  17896  isfull2  18068  isfth2  18072  ecxpid  19366  isghm3  19411  gastacos  19504  sylow2alem2  19812  lssnle  19868  isabl2  19984  submcmn2  20033  iscyggen2  20075  iscyg3  20080  cyggexb  20093  gsum2d2  20168  dprdw  20206  dprd2da  20238  iscrng2  20459  dvdsr2  20573  dfrhm2  20684  brric2  20734  isdomn2  20943  sdrgacs  21038  islmhm3  21283  ssdifidlprm  21622  prmirredlem  21758  chrnzr  21816  iunocv  21967  iscss2  21972  ishil2  22005  obselocv  22014  psrbaglefi  22214  mplsubrglem  22291  bastop1  23291  isclo  23385  maxlp  23445  isperf2  23450  restperf  23482  cnpnei  23562  cnntr  23573  cnprest  23587  cnprest2  23588  lmres  23598  iscnrm2  23636  ist0-2  23642  ist1-2  23645  ishaus2  23649  tgcmp  23699  cmpfi  23706  dfconn2  23717  t1connperf  23734  subislly  23780  tx1cn  23908  tx2cn  23909  xkopt  23954  xkoinjcn  23986  ist0-4  24028  trfil2  24186  fin1aufil  24231  flimtopon  24269  elflim  24270  fclstopon  24311  isfcls2  24312  alexsubALTlem4  24349  ptcmplem3  24353  tgphaus  24416  xmetec  24733  prdsbl  24790  blval2  24861  isnvc2  24998  isnghm2  25023  isnmhm2  25051  0nmhm  25054  xrtgioo  25106  cncfcnvcn  25226  evth  25260  nmhmcn  25421  cmsss  25652  lssbn  25653  srabn  25661  ishl2  25671  ivthlem2  25753  0plef  25973  itg2monolem1  26051  itg2cnlem1  26062  itg2cnlem2  26063  ellimc2  26177  dvne0  26311  ellogdm  26949  dcubic  27156  atans2  27241  amgm  27300  ftalem3  27384  pclogsum  27524  dchrelbas3  27547  lgsabs1  27645  dchrvmaeq0  27813  rpvmasum2  27821  tgjustf  28917  lfuhgr  29708  clwwlkwwlksb  30627  ajval  31445  bnsscmcl  31452  axhcompl-zf  31582  seq1hcau  31771  hlim2  31776  issh3  31803  lnopcnre  32623  dmdbr2  32887  elatcv0  32925  iunsnima  33194  iunsnima2  33195  partfun2  33252  ist0cld  34447  1stmbfm  34875  2ndmbfm  34876  eulerpartlemd  34981  oddprm2  35267  scottrankeqel  35726  cvmlift2lem12  36048  bj-rest10  37977  topdifinfeq  38241  finxpsuclem  38288  curunc  38493  istotbnd2  38672  sstotbnd2  38676  isbnd3b  38687  totbndbnd  38691  br1cnvres  39174  fimgmcyc  43560  islnr2  44074  areaquad  44176  tfsconcat0i  44305  afv2res  48253  oddm1evenALTV  48717  oddp1evenALTV  48718  crngprmringdom  49383  iscnrm3v  50005  isprsd  50007  joindm2  50020  meetdm2  50022  postcposALT  50620  postc  50621  dvsec  50800  dvcsc  50801  dvcot  50802