Theorem baib 536

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  baibr  537  ceqsrexbv  3644  elrab3  3684  dfpss3  4086  rabsn  4725  elrint2  4996  opres  5991  cores  6248  fnres  6677  fvres  6910  fvmpti  6997  f1ompt  7112  fliftfun  7311  isocnv3  7331  riotaxfrd  7402  ovid  7551  nlimon  7842  limom  7873  brdifun  8734  xpcomco  9064  0sdomg  9106  0sdomgOLD  9107  f1finf1o  9273  f1finf1oOLD  9274  ordtypelem9  9523  isacn  10041  alephinit  10092  isfin5-2  10388  pwfseqlem1  10655  pwfseqlem3  10657  pwfseqlem4  10659  ltresr  11137  xrlenlt  11281  znnnlt1  12591  difrp  13014  elfz  13492  fzolb2  13641  elfzo3  13651  fzouzsplit  13669  rabssnn0fi  13953  caubnd  15307  ello12  15462  elo12  15473  bitsval2  16368  smueqlem  16433  rpexp  16661  ramcl  16964  ismon2  17683  isepi2  17690  isfull2  17864  isfth2  17868  isghm3  19095  gastacos  19176  sylow2alem2  19488  lssnle  19544  isabl2  19660  submcmn2  19709  iscyggen2  19751  iscyg3  19756  cyggexb  19769  gsum2d2  19844  dprdw  19882  dprd2da  19914  iscrng2  20077  dvdsr2  20181  dfrhm2  20257  sdrgacs  20421  islmhm3  20644  isdomn2  20921  prmirredlem  21048  chrnzr  21088  iunocv  21240  iscss2  21245  ishil2  21280  obselocv  21289  psrbaglefi  21491  psrbaglefiOLD  21492  mplsubrglem  21569  bastop1  22503  isclo  22598  maxlp  22658  isperf2  22663  restperf  22695  cnpnei  22775  cnntr  22786  cnprest  22800  cnprest2  22801  lmres  22811  iscnrm2  22849  ist0-2  22855  ist1-2  22858  ishaus2  22862  tgcmp  22912  cmpfi  22919  dfconn2  22930  t1connperf  22947  subislly  22992  tx1cn  23120  tx2cn  23121  xkopt  23166  xkoinjcn  23198  ist0-4  23240  trfil2  23398  fin1aufil  23443  flimtopon  23481  elflim  23482  fclstopon  23523  isfcls2  23524  alexsubALTlem4  23561  ptcmplem3  23565  tgphaus  23628  xmetec  23947  prdsbl  24007  blval2  24078  isnvc2  24223  isnghm2  24248  isnmhm2  24276  0nmhm  24279  xrtgioo  24329  cncfcnvcn  24448  evth  24482  nmhmcn  24643  cmsss  24875  lssbn  24876  srabn  24884  ishl2  24894  ivthlem2  24976  0plef  25196  itg2monolem1  25275  itg2cnlem1  25286  itg2cnlem2  25287  ellimc2  25401  dvne0  25535  ellogdm  26154  dcubic  26358  atans2  26443  amgm  26502  ftalem3  26586  pclogsum  26725  dchrelbas3  26748  lgsabs1  26846  dchrvmaeq0  27014  rpvmasum2  27022  tgjustf  27762  clwwlkwwlksb  29345  ajval  30152  bnsscmcl  30159  axhcompl-zf  30289  seq1hcau  30478  hlim2  30483  issh3  30510  lnopcnre  31330  dmdbr2  31594  elatcv0  31632  iunsnima  31885  iunsnima2  31886  ecxpid  32517  ist0cld  32882  1stmbfm  33328  2ndmbfm  33329  eulerpartlemd  33434  oddprm2  33736  lfuhgr  34177  cvmlift2lem12  34374  bj-rest10  36061  topdifinfeq  36323  finxpsuclem  36370  curunc  36562  istotbnd2  36730  sstotbnd2  36734  isbnd3b  36745  totbndbnd  36749  br1cnvres  37229  ecres2  37239  islnr2  41944  areaquad  42053  tfsconcat0i  42183  afv2res  46032  oddm1evenALTV  46428  oddp1evenALTV  46429  iscnrm3v  47670  isprsd  47672  joindm2  47685  meetdm2  47687  postcposALT  47785  postc  47786