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  3553  elrab3  3589  dfpss3  3977  rabsn  4612  elrint2  4880  opres  5835  cores  6082  elpredg  6143  fnres  6463  fvres  6693  fvmpti  6774  f1ompt  6885  fliftfun  7078  isocnv3  7098  riotaxfrd  7162  ovid  7306  nlimon  7585  limom  7614  brdifun  8349  xpcomco  8656  0sdomg  8696  f1finf1o  8823  ordtypelem9  9063  isacn  9544  alephinit  9595  isfin5-2  9891  pwfseqlem1  10158  pwfseqlem3  10160  pwfseqlem4  10162  ltresr  10640  xrlenlt  10784  znnnlt1  12090  difrp  12510  elfz  12987  fzolb2  13136  elfzo3  13145  fzouzsplit  13163  rabssnn0fi  13445  caubnd  14808  ello12  14963  elo12  14974  bitsval2  15868  smueqlem  15933  rpexp  16163  ramcl  16465  ismon2  17109  isepi2  17116  isfull2  17286  isfth2  17290  isghm3  18477  gastacos  18558  sylow2alem2  18861  lssnle  18918  isabl2  19033  submcmn2  19078  iscyggen2  19119  iscyg3  19124  cyggexb  19138  gsum2d2  19213  dprdw  19251  dprd2da  19283  iscrng2  19435  dvdsr2  19519  dfrhm2  19591  sdrgacs  19699  islmhm3  19919  isdomn2  20191  prmirredlem  20313  chrnzr  20349  iunocv  20497  iscss2  20502  ishil2  20535  obselocv  20544  psrbaglefi  20745  psrbaglefiOLD  20746  mplsubrglem  20820  bastop1  21744  isclo  21838  maxlp  21898  isperf2  21903  restperf  21935  cnpnei  22015  cnntr  22026  cnprest  22040  cnprest2  22041  lmres  22051  iscnrm2  22089  ist0-2  22095  ist1-2  22098  ishaus2  22102  tgcmp  22152  cmpfi  22159  dfconn2  22170  t1connperf  22187  subislly  22232  tx1cn  22360  tx2cn  22361  xkopt  22406  xkoinjcn  22438  ist0-4  22480  trfil2  22638  fin1aufil  22683  flimtopon  22721  elflim  22722  fclstopon  22763  isfcls2  22764  alexsubALTlem4  22801  ptcmplem3  22805  tgphaus  22868  xmetec  23187  prdsbl  23244  blval2  23315  isnvc2  23452  isnghm2  23477  isnmhm2  23505  0nmhm  23508  xrtgioo  23558  cncfcnvcn  23677  evth  23711  nmhmcn  23872  cmsss  24103  lssbn  24104  srabn  24112  ishl2  24122  ivthlem2  24204  0plef  24424  itg2monolem1  24503  itg2cnlem1  24514  itg2cnlem2  24515  ellimc2  24629  dvne0  24763  ellogdm  25382  dcubic  25584  atans2  25669  amgm  25728  ftalem3  25812  pclogsum  25951  dchrelbas3  25974  lgsabs1  26072  dchrvmaeq0  26240  rpvmasum2  26248  tgjustf  26419  clwwlkwwlksb  27991  ajval  28796  bnsscmcl  28803  axhcompl-zf  28933  seq1hcau  29122  hlim2  29127  issh3  29154  lnopcnre  29974  dmdbr2  30238  elatcv0  30276  iunsnima  30532  iunsnima2  30533  ecxpid  31128  ist0cld  31355  1stmbfm  31797  2ndmbfm  31798  eulerpartlemd  31903  oddprm2  32205  lfuhgr  32650  cvmlift2lem12  32847  bj-rest10  34880  topdifinfeq  35144  finxpsuclem  35191  curunc  35382  istotbnd2  35551  sstotbnd2  35555  isbnd3b  35566  totbndbnd  35570  ecres2  36037  islnr2  40511  areaquad  40619  afv2res  44264  oddm1evenALTV  44661  oddp1evenALTV  44662  iscnrm3v  45769  isprsd  45771