Theorem baib 544

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

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

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 401

This theorem is referenced by:  baibr  545  ceqsrexbv  3618  elrab3  3654  dfpss3  4045  rabsn  4683  elrint2  4951  opres  5979  cores  6240  fnres  6652  fvres  6890  fvmpti  6978  f1ompt  7096  fliftfun  7300  isocnv3  7320  riotaxfrd  7391  ovid  7541  nlimon  7835  limom  7866  brdifun  8713  elecreseq  8732  xpcomco  9043  0sdomg  9082  f1finf1o  9221  ordtypelem9  9476  isacn  10016  alephinit  10067  isfin5-2  10363  pwfseqlem1  10631  pwfseqlem3  10633  pwfseqlem4  10635  ltresr  11113  xrlenlt  11262  znnnlt1  12612  difrp  13047  elfz  13532  fzolb2  13686  elfzo3  13696  fzouzsplit  13714  rabssnn0fi  14013  caubnd  15400  ello12  15557  elo12  15568  bitsval2  16473  smueqlem  16538  rpexp  16771  ramcl  17079  ismon2  17781  isepi2  17788  isfull2  17960  isfth2  17964  ecxpid  19233  isghm3  19278  gastacos  19371  sylow2alem2  19679  lssnle  19735  isabl2  19851  submcmn2  19900  iscyggen2  19942  iscyg3  19947  cyggexb  19960  gsum2d2  20035  dprdw  20073  dprd2da  20105  iscrng2  20325  dvdsr2  20436  dfrhm2  20547  isdomn2  20787  sdrgacs  20873  islmhm3  21118  ssdifidlprm  21446  prmirredlem  21582  chrnzr  21640  iunocv  21791  iscss2  21796  ishil2  21829  obselocv  21838  psrbaglefi  22036  mplsubrglem  22113  bastop1  23111  isclo  23205  maxlp  23265  isperf2  23270  restperf  23302  cnpnei  23382  cnntr  23393  cnprest  23407  cnprest2  23408  lmres  23418  iscnrm2  23456  ist0-2  23462  ist1-2  23465  ishaus2  23469  tgcmp  23519  cmpfi  23526  dfconn2  23537  t1connperf  23554  subislly  23599  tx1cn  23727  tx2cn  23728  xkopt  23773  xkoinjcn  23805  ist0-4  23847  trfil2  24005  fin1aufil  24050  flimtopon  24088  elflim  24089  fclstopon  24130  isfcls2  24131  alexsubALTlem4  24168  ptcmplem3  24172  tgphaus  24235  xmetec  24552  prdsbl  24609  blval2  24680  isnvc2  24817  isnghm2  24842  isnmhm2  24870  0nmhm  24873  xrtgioo  24925  cncfcnvcn  25045  evth  25079  nmhmcn  25240  cmsss  25471  lssbn  25472  srabn  25480  ishl2  25490  ivthlem2  25572  0plef  25792  itg2monolem1  25870  itg2cnlem1  25881  itg2cnlem2  25882  ellimc2  25997  dvne0  26131  ellogdm  26762  dcubic  26969  atans2  27054  amgm  27113  ftalem3  27197  pclogsum  27337  dchrelbas3  27360  lgsabs1  27458  dchrvmaeq0  27626  rpvmasum2  27634  tgjustf  28700  clwwlkwwlksb  30314  ajval  31122  bnsscmcl  31129  axhcompl-zf  31259  seq1hcau  31448  hlim2  31453  issh3  31480  lnopcnre  32300  dmdbr2  32564  elatcv0  32602  iunsnima  32875  iunsnima2  32876  partfun2  32933  ist0cld  34140  1stmbfm  34567  2ndmbfm  34568  eulerpartlemd  34673  oddprm2  34959  lfuhgr  35481  cvmlift2lem12  35677  bj-rest10  37590  topdifinfeq  37856  finxpsuclem  37903  curunc  38113  istotbnd2  38281  sstotbnd2  38285  isbnd3b  38296  totbndbnd  38300  br1cnvres  38785  fimgmcyc  43164  islnr2  43703  areaquad  43805  tfsconcat0i  43934  afv2res  47831  oddm1evenALTV  48295  oddp1evenALTV  48296  crngprmringdom  48962  iscnrm3v  49582  isprsd  49584  joindm2  49597  meetdm2  49599  postcposALT  50197  postc  50198