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  3655  elrab3  3695  dfpss3  4098  rabsn  4725  elrint2  4994  opres  6009  cores  6270  fnres  6695  fvres  6925  fvmpti  7014  f1ompt  7130  fliftfun  7331  isocnv3  7351  riotaxfrd  7421  ovid  7573  nlimon  7871  limom  7902  brdifun  8773  xpcomco  9100  0sdomg  9142  0sdomgOLD  9143  f1finf1o  9302  f1finf1oOLD  9303  ordtypelem9  9563  isacn  10081  alephinit  10132  isfin5-2  10428  pwfseqlem1  10695  pwfseqlem3  10697  pwfseqlem4  10699  ltresr  11177  xrlenlt  11323  znnnlt1  12641  difrp  13070  elfz  13549  fzolb2  13702  elfzo3  13712  fzouzsplit  13730  rabssnn0fi  14023  caubnd  15393  ello12  15548  elo12  15559  bitsval2  16458  smueqlem  16523  rpexp  16755  ramcl  17062  ismon2  17781  isepi2  17788  isfull2  17964  isfth2  17968  isghm3  19247  gastacos  19340  sylow2alem2  19650  lssnle  19706  isabl2  19822  submcmn2  19871  iscyggen2  19913  iscyg3  19918  cyggexb  19931  gsum2d2  20006  dprdw  20044  dprd2da  20076  iscrng2  20269  dvdsr2  20379  dfrhm2  20490  isdomn2  20727  isdomn2OLD  20728  sdrgacs  20818  islmhm3  21044  prmirredlem  21500  chrnzr  21562  iunocv  21716  iscss2  21721  ishil2  21756  obselocv  21765  psrbaglefi  21963  mplsubrglem  22041  bastop1  23015  isclo  23110  maxlp  23170  isperf2  23175  restperf  23207  cnpnei  23287  cnntr  23298  cnprest  23312  cnprest2  23313  lmres  23323  iscnrm2  23361  ist0-2  23367  ist1-2  23370  ishaus2  23374  tgcmp  23424  cmpfi  23431  dfconn2  23442  t1connperf  23459  subislly  23504  tx1cn  23632  tx2cn  23633  xkopt  23678  xkoinjcn  23710  ist0-4  23752  trfil2  23910  fin1aufil  23955  flimtopon  23993  elflim  23994  fclstopon  24035  isfcls2  24036  alexsubALTlem4  24073  ptcmplem3  24077  tgphaus  24140  xmetec  24459  prdsbl  24519  blval2  24590  isnvc2  24735  isnghm2  24760  isnmhm2  24788  0nmhm  24791  xrtgioo  24841  cncfcnvcn  24965  evth  25004  nmhmcn  25166  cmsss  25398  lssbn  25399  srabn  25407  ishl2  25417  ivthlem2  25500  0plef  25720  itg2monolem1  25799  itg2cnlem1  25810  itg2cnlem2  25811  ellimc2  25926  dvne0  26064  ellogdm  26695  dcubic  26903  atans2  26988  amgm  27048  ftalem3  27132  pclogsum  27273  dchrelbas3  27296  lgsabs1  27394  dchrvmaeq0  27562  rpvmasum2  27570  tgjustf  28495  clwwlkwwlksb  30082  ajval  30889  bnsscmcl  30896  axhcompl-zf  31026  seq1hcau  31215  hlim2  31220  issh3  31247  lnopcnre  32067  dmdbr2  32331  elatcv0  32369  iunsnima  32637  iunsnima2  32638  ecxpid  33368  ssdifidlprm  33465  ist0cld  33793  1stmbfm  34241  2ndmbfm  34242  eulerpartlemd  34347  oddprm2  34648  lfuhgr  35101  cvmlift2lem12  35298  bj-rest10  37070  topdifinfeq  37332  finxpsuclem  37379  curunc  37588  istotbnd2  37756  sstotbnd2  37760  isbnd3b  37771  totbndbnd  37775  br1cnvres  38250  ecres2  38260  fimgmcyc  42520  islnr2  43102  areaquad  43204  tfsconcat0i  43334  afv2res  47188  oddm1evenALTV  47599  oddp1evenALTV  47600  iscnrm3v  48749  isprsd  48751  joindm2  48764  meetdm2  48766  postcposALT  48883  postc  48884