Theorem baib 545

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  baibr  546  ceqsrexbv  3613  elrab3  3649  dfpss3  4019  rabsn  4682  elrint2  4953  opres  5992  cores  6264  fnres  6691  fvres  6930  fvmpti  7018  f1ompt  7138  fliftfun  7346  isocnv3  7366  riotaxfrd  7437  ovid  7588  nlimon  7889  limom  7920  brdifun  8779  elecreseq  8798  xpcomco  9117  0sdomg  9156  f1finf1o  9295  ordtypelem9  9550  isacn  10153  alephinit  10204  isfin5-2  10499  pwfseqlem1  10773  pwfseqlem3  10775  pwfseqlem4  10777  ltresr  11255  xrlenlt  11404  znnnlt1  12753  difrp  13190  elfz  13675  fzolb2  13831  elfzo3  13841  fzouzsplit  13859  rabssnn0fi  14159  caubnd  15558  ello12  15715  elo12  15726  bitsval2  16627  smueqlem  16692  rpexp  16930  ramcl  17239  ismon2  17941  isepi2  17948  isfull2  18120  isfth2  18124  ecxpid  19418  isghm3  19463  gastacos  19557  sylow2alem2  19865  lssnle  19921  isabl2  20037  submcmn2  20086  iscyggen2  20128  iscyg3  20133  cyggexb  20146  gsum2d2  20221  dprdw  20259  dprd2da  20291  iscrng2  20512  dvdsr2  20626  dfrhm2  20737  brric2  20787  isdomn2  20996  sdrgacs  21091  islmhm3  21336  ssdifidlprm  21675  prmirredlem  21811  chrnzr  21869  iunocv  22020  iscss2  22025  ishil2  22058  obselocv  22067  psrbaglefi  22267  mplsubrglem  22344  bastop1  23344  isclo  23438  maxlp  23498  isperf2  23503  restperf  23535  cnpnei  23615  cnntr  23626  cnprest  23640  cnprest2  23641  lmres  23651  iscnrm2  23689  ist0-2  23695  ist1-2  23698  ishaus2  23702  tgcmp  23752  cmpfi  23759  dfconn2  23770  t1connperf  23787  subislly  23833  tx1cn  23961  tx2cn  23962  xkopt  24007  xkoinjcn  24039  ist0-4  24081  trfil2  24239  fin1aufil  24284  flimtopon  24322  elflim  24323  fclstopon  24364  isfcls2  24365  alexsubALTlem4  24402  ptcmplem3  24406  tgphaus  24469  xmetec  24786  prdsbl  24843  blval2  24914  isnvc2  25051  isnghm2  25076  isnmhm2  25104  0nmhm  25107  xrtgioo  25159  cncfcnvcn  25279  evth  25313  nmhmcn  25474  cmsss  25705  lssbn  25706  srabn  25714  ishl2  25724  ivthlem2  25806  0plef  26026  itg2monolem1  26104  itg2cnlem1  26115  itg2cnlem2  26116  ellimc2  26230  dvne0  26364  ellogdm  27000  dcubic  27207  atans2  27292  amgm  27351  ftalem3  27435  pclogsum  27575  dchrelbas3  27598  lgsabs1  27696  dchrvmaeq0  27864  rpvmasum2  27872  tgjustf  28968  lfuhgr  29759  clwwlkwwlksb  30678  ajval  31496  bnsscmcl  31503  axhcompl-zf  31633  seq1hcau  31822  hlim2  31827  issh3  31854  lnopcnre  32674  dmdbr2  32938  elatcv0  32976  iunsnima  33287  iunsnima2  33288  partfun2  33344  ist0cld  34548  1stmbfm  34975  2ndmbfm  34976  eulerpartlemd  35081  oddprm2  35367  fwfffunres  35801  scottrankeqel  35845  cvmlift2lem12  36259  bj-rest10  38213  topdifinfeq  38478  finxpsuclem  38525  curunc  38730  istotbnd2  38907  sstotbnd2  38911  isbnd3b  38922  totbndbnd  38926  br1cnvres  39409  fimgmcyc  43802  islnr2  44319  areaquad  44421  tfsconcat0i  44550  afv2res  48524  oddm1evenALTV  48988  oddp1evenALTV  48989  crngprmringdom  49654  iscnrm3v  50282  isprsd  50284  joindm2  50297  meetdm2  50299  postcposALT  50921  postc  50922  dvsec  51168  dvcsc  51169  dvcot  51170