Theorem baib 539

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  baibr  540  ceqsrexbv  3598  elrab3  3629  dfpss3  4014  rabsn  4617  elrint2  4880  opres  5828  cores  6069  elpredg  6130  fnres  6446  fvres  6664  fvmpti  6744  f1ompt  6852  fliftfun  7044  isocnv3  7064  riotaxfrd  7127  ovid  7270  nlimon  7546  limom  7575  brdifun  8301  xpcomco  8590  0sdomg  8630  f1finf1o  8729  ordtypelem9  8974  isacn  9455  alephinit  9506  isfin5-2  9802  pwfseqlem1  10069  pwfseqlem3  10071  pwfseqlem4  10073  ltresr  10551  xrlenlt  10695  znnnlt1  11997  difrp  12415  elfz  12891  fzolb2  13040  elfzo3  13049  fzouzsplit  13067  rabssnn0fi  13349  caubnd  14710  ello12  14865  elo12  14876  bitsval2  15764  smueqlem  15829  rpexp  16054  ramcl  16355  ismon2  16996  isepi2  17003  isfull2  17173  isfth2  17177  isghm3  18351  gastacos  18432  sylow2alem2  18735  lssnle  18792  isabl2  18907  submcmn2  18952  iscyggen2  18993  iscyg3  18998  cyggexb  19012  gsum2d2  19087  dprdw  19125  dprd2da  19157  iscrng2  19309  dvdsr2  19393  dfrhm2  19465  sdrgacs  19573  islmhm3  19793  isdomn2  20065  prmirredlem  20186  chrnzr  20222  iunocv  20370  iscss2  20375  ishil2  20408  obselocv  20417  psrbaglefi  20610  mplsubrglem  20677  bastop1  21598  isclo  21692  maxlp  21752  isperf2  21757  restperf  21789  cnpnei  21869  cnntr  21880  cnprest  21894  cnprest2  21895  lmres  21905  iscnrm2  21943  ist0-2  21949  ist1-2  21952  ishaus2  21956  tgcmp  22006  cmpfi  22013  dfconn2  22024  t1connperf  22041  subislly  22086  tx1cn  22214  tx2cn  22215  xkopt  22260  xkoinjcn  22292  ist0-4  22334  trfil2  22492  fin1aufil  22537  flimtopon  22575  elflim  22576  fclstopon  22617  isfcls2  22618  alexsubALTlem4  22655  ptcmplem3  22659  tgphaus  22722  xmetec  23041  prdsbl  23098  blval2  23169  isnvc2  23305  isnghm2  23330  isnmhm2  23358  0nmhm  23361  xrtgioo  23411  cncfcnvcn  23530  evth  23564  nmhmcn  23725  cmsss  23955  lssbn  23956  srabn  23964  ishl2  23974  ivthlem2  24056  0plef  24276  itg2monolem1  24354  itg2cnlem1  24365  itg2cnlem2  24366  ellimc2  24480  dvne0  24614  ellogdm  25230  dcubic  25432  atans2  25517  amgm  25576  ftalem3  25660  pclogsum  25799  dchrelbas3  25822  lgsabs1  25920  dchrvmaeq0  26088  rpvmasum2  26096  tgjustf  26267  clwwlkwwlksb  27839  ajval  28644  bnsscmcl  28651  axhcompl-zf  28781  seq1hcau  28970  hlim2  28975  issh3  29002  lnopcnre  29822  dmdbr2  30086  elatcv0  30124  iunsnima  30382  iunsnima2  30383  ecxpid  30976  ist0cld  31186  1stmbfm  31628  2ndmbfm  31629  eulerpartlemd  31734  oddprm2  32036  lfuhgr  32477  cvmlift2lem12  32674  bj-rest10  34503  topdifinfeq  34767  finxpsuclem  34814  curunc  35039  istotbnd2  35208  sstotbnd2  35212  isbnd3b  35223  totbndbnd  35227  ecres2  35696  islnr2  40058  areaquad  40166  afv2res  43795  oddm1evenALTV  44193  oddp1evenALTV  44194