Theorem baib 535

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  baibr  536  ceqsrexbv  3612  elrab3  3649  dfpss3  4043  rabsn  4680  elrint2  4947  opres  5956  cores  6215  fnres  6627  fvres  6861  fvmpti  6948  f1ompt  7065  fliftfun  7268  isocnv3  7288  riotaxfrd  7359  ovid  7509  nlimon  7803  limom  7834  brdifun  8676  elecreseq  8695  xpcomco  9007  0sdomg  9046  f1finf1o  9185  ordtypelem9  9443  isacn  9966  alephinit  10017  isfin5-2  10313  pwfseqlem1  10581  pwfseqlem3  10583  pwfseqlem4  10585  ltresr  11063  xrlenlt  11209  znnnlt1  12530  difrp  12957  elfz  13441  fzolb2  13594  elfzo3  13604  fzouzsplit  13622  rabssnn0fi  13921  caubnd  15294  ello12  15451  elo12  15462  bitsval2  16364  smueqlem  16429  rpexp  16661  ramcl  16969  ismon2  17670  isepi2  17677  isfull2  17849  isfth2  17853  isghm3  19158  gastacos  19251  sylow2alem2  19559  lssnle  19615  isabl2  19731  submcmn2  19780  iscyggen2  19822  iscyg3  19827  cyggexb  19840  gsum2d2  19915  dprdw  19953  dprd2da  19985  iscrng2  20199  dvdsr2  20311  dfrhm2  20422  isdomn2  20656  isdomn2OLD  20657  sdrgacs  20746  islmhm3  20992  prmirredlem  21439  chrnzr  21497  iunocv  21648  iscss2  21653  ishil2  21686  obselocv  21695  psrbaglefi  21894  mplsubrglem  21971  bastop1  22949  isclo  23043  maxlp  23103  isperf2  23108  restperf  23140  cnpnei  23220  cnntr  23231  cnprest  23245  cnprest2  23246  lmres  23256  iscnrm2  23294  ist0-2  23300  ist1-2  23303  ishaus2  23307  tgcmp  23357  cmpfi  23364  dfconn2  23375  t1connperf  23392  subislly  23437  tx1cn  23565  tx2cn  23566  xkopt  23611  xkoinjcn  23643  ist0-4  23685  trfil2  23843  fin1aufil  23888  flimtopon  23926  elflim  23927  fclstopon  23968  isfcls2  23969  alexsubALTlem4  24006  ptcmplem3  24010  tgphaus  24073  xmetec  24390  prdsbl  24447  blval2  24518  isnvc2  24655  isnghm2  24680  isnmhm2  24708  0nmhm  24711  xrtgioo  24763  cncfcnvcn  24887  evth  24926  nmhmcn  25088  cmsss  25319  lssbn  25320  srabn  25328  ishl2  25338  ivthlem2  25421  0plef  25641  itg2monolem1  25719  itg2cnlem1  25730  itg2cnlem2  25731  ellimc2  25846  dvne0  25984  ellogdm  26616  dcubic  26824  atans2  26909  amgm  26969  ftalem3  27053  pclogsum  27194  dchrelbas3  27217  lgsabs1  27315  dchrvmaeq0  27483  rpvmasum2  27491  tgjustf  28557  clwwlkwwlksb  30141  ajval  30948  bnsscmcl  30955  axhcompl-zf  31085  seq1hcau  31274  hlim2  31279  issh3  31306  lnopcnre  32126  dmdbr2  32390  elatcv0  32428  iunsnima  32707  iunsnima2  32708  partfun2  32765  ecxpid  33453  ssdifidlprm  33550  ist0cld  34010  1stmbfm  34437  2ndmbfm  34438  eulerpartlemd  34543  oddprm2  34832  lfuhgr  35331  cvmlift2lem12  35527  bj-rest10  37335  topdifinfeq  37599  finxpsuclem  37646  curunc  37847  istotbnd2  38015  sstotbnd2  38019  isbnd3b  38030  totbndbnd  38034  br1cnvres  38519  fimgmcyc  42898  islnr2  43465  areaquad  43567  tfsconcat0i  43696  afv2res  47593  oddm1evenALTV  48029  oddp1evenALTV  48030  iscnrm3v  49306  isprsd  49308  joindm2  49321  meetdm2  49323  postcposALT  49921  postc  49922