Theorem baib 540

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  baibr  541  ceqsrexbv  3601  elrab3  3637  dfpss3  4027  rabsn  4660  elrint2  4927  opres  5948  cores  6207  fnres  6619  fvres  6853  fvmpti  6941  f1ompt  7059  fliftfun  7263  isocnv3  7283  riotaxfrd  7354  ovid  7504  nlimon  7798  limom  7829  brdifun  8671  elecreseq  8690  xpcomco  9002  0sdomg  9041  f1finf1o  9180  ordtypelem9  9438  isacn  9964  alephinit  10015  isfin5-2  10311  pwfseqlem1  10579  pwfseqlem3  10581  pwfseqlem4  10583  ltresr  11061  xrlenlt  11208  znnnlt1  12552  difrp  12980  elfz  13465  fzolb2  13619  elfzo3  13629  fzouzsplit  13647  rabssnn0fi  13946  caubnd  15319  ello12  15476  elo12  15487  bitsval2  16392  smueqlem  16457  rpexp  16690  ramcl  16998  ismon2  17699  isepi2  17706  isfull2  17878  isfth2  17882  isghm3  19190  gastacos  19283  sylow2alem2  19591  lssnle  19647  isabl2  19763  submcmn2  19812  iscyggen2  19854  iscyg3  19859  cyggexb  19872  gsum2d2  19947  dprdw  19985  dprd2da  20017  iscrng2  20231  dvdsr2  20341  dfrhm2  20452  isdomn2  20690  isdomn2OLD  20691  sdrgacs  20780  islmhm3  21025  prmirredlem  21454  chrnzr  21512  iunocv  21663  iscss2  21668  ishil2  21701  obselocv  21710  psrbaglefi  21908  mplsubrglem  21985  bastop1  22983  isclo  23077  maxlp  23137  isperf2  23142  restperf  23174  cnpnei  23254  cnntr  23265  cnprest  23279  cnprest2  23280  lmres  23290  iscnrm2  23328  ist0-2  23334  ist1-2  23337  ishaus2  23341  tgcmp  23391  cmpfi  23398  dfconn2  23409  t1connperf  23426  subislly  23471  tx1cn  23599  tx2cn  23600  xkopt  23645  xkoinjcn  23677  ist0-4  23719  trfil2  23877  fin1aufil  23922  flimtopon  23960  elflim  23961  fclstopon  24002  isfcls2  24003  alexsubALTlem4  24040  ptcmplem3  24044  tgphaus  24107  xmetec  24424  prdsbl  24481  blval2  24552  isnvc2  24689  isnghm2  24714  isnmhm2  24742  0nmhm  24745  xrtgioo  24797  cncfcnvcn  24917  evth  24951  nmhmcn  25112  cmsss  25343  lssbn  25344  srabn  25352  ishl2  25362  ivthlem2  25444  0plef  25664  itg2monolem1  25742  itg2cnlem1  25753  itg2cnlem2  25754  ellimc2  25869  dvne0  26003  ellogdm  26628  dcubic  26835  atans2  26920  amgm  26979  ftalem3  27063  pclogsum  27203  dchrelbas3  27226  lgsabs1  27324  dchrvmaeq0  27492  rpvmasum2  27500  tgjustf  28566  clwwlkwwlksb  30149  ajval  30957  bnsscmcl  30964  axhcompl-zf  31094  seq1hcau  31283  hlim2  31288  issh3  31315  lnopcnre  32135  dmdbr2  32399  elatcv0  32437  iunsnima  32717  iunsnima2  32718  partfun2  32775  ecxpid  33451  ssdifidlprm  33548  ist0cld  34024  1stmbfm  34451  2ndmbfm  34452  eulerpartlemd  34557  oddprm2  34846  lfuhgr  35353  cvmlift2lem12  35549  bj-rest10  37453  topdifinfeq  37719  finxpsuclem  37766  curunc  37976  istotbnd2  38144  sstotbnd2  38148  isbnd3b  38159  totbndbnd  38163  br1cnvres  38648  fimgmcyc  43027  islnr2  43566  areaquad  43668  tfsconcat0i  43797  afv2res  47709  oddm1evenALTV  48173  oddp1evenALTV  48174  iscnrm3v  49450  isprsd  49452  joindm2  49465  meetdm2  49467  postcposALT  50065  postc  50066