Theorem baib 535

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  baibr  536  ceqsrexbv  3613  elrab3  3651  dfpss3  4042  rabsn  4675  elrint2  4943  opres  5944  cores  6202  fnres  6613  fvres  6845  fvmpti  6933  f1ompt  7049  fliftfun  7253  isocnv3  7273  riotaxfrd  7344  ovid  7494  nlimon  7791  limom  7822  brdifun  8662  elecreseq  8681  xpcomco  8991  0sdomg  9030  f1finf1o  9174  f1finf1oOLD  9175  ordtypelem9  9437  isacn  9957  alephinit  10008  isfin5-2  10304  pwfseqlem1  10571  pwfseqlem3  10573  pwfseqlem4  10575  ltresr  11053  xrlenlt  11199  znnnlt1  12520  difrp  12951  elfz  13434  fzolb2  13587  elfzo3  13597  fzouzsplit  13615  rabssnn0fi  13911  caubnd  15284  ello12  15441  elo12  15452  bitsval2  16354  smueqlem  16419  rpexp  16651  ramcl  16959  ismon2  17659  isepi2  17666  isfull2  17838  isfth2  17842  isghm3  19114  gastacos  19207  sylow2alem2  19515  lssnle  19571  isabl2  19687  submcmn2  19736  iscyggen2  19778  iscyg3  19783  cyggexb  19796  gsum2d2  19871  dprdw  19909  dprd2da  19941  iscrng2  20155  dvdsr2  20266  dfrhm2  20377  isdomn2  20614  isdomn2OLD  20615  sdrgacs  20704  islmhm3  20950  prmirredlem  21397  chrnzr  21455  iunocv  21606  iscss2  21611  ishil2  21644  obselocv  21653  psrbaglefi  21851  mplsubrglem  21929  bastop1  22896  isclo  22990  maxlp  23050  isperf2  23055  restperf  23087  cnpnei  23167  cnntr  23178  cnprest  23192  cnprest2  23193  lmres  23203  iscnrm2  23241  ist0-2  23247  ist1-2  23250  ishaus2  23254  tgcmp  23304  cmpfi  23311  dfconn2  23322  t1connperf  23339  subislly  23384  tx1cn  23512  tx2cn  23513  xkopt  23558  xkoinjcn  23590  ist0-4  23632  trfil2  23790  fin1aufil  23835  flimtopon  23873  elflim  23874  fclstopon  23915  isfcls2  23916  alexsubALTlem4  23953  ptcmplem3  23957  tgphaus  24020  xmetec  24338  prdsbl  24395  blval2  24466  isnvc2  24603  isnghm2  24628  isnmhm2  24656  0nmhm  24659  xrtgioo  24711  cncfcnvcn  24835  evth  24874  nmhmcn  25036  cmsss  25267  lssbn  25268  srabn  25276  ishl2  25286  ivthlem2  25369  0plef  25589  itg2monolem1  25667  itg2cnlem1  25678  itg2cnlem2  25679  ellimc2  25794  dvne0  25932  ellogdm  26564  dcubic  26772  atans2  26857  amgm  26917  ftalem3  27001  pclogsum  27142  dchrelbas3  27165  lgsabs1  27263  dchrvmaeq0  27431  rpvmasum2  27439  tgjustf  28436  clwwlkwwlksb  30016  ajval  30823  bnsscmcl  30830  axhcompl-zf  30960  seq1hcau  31149  hlim2  31154  issh3  31181  lnopcnre  32001  dmdbr2  32265  elatcv0  32303  iunsnima  32579  iunsnima2  32580  ecxpid  33308  ssdifidlprm  33405  ist0cld  33799  1stmbfm  34227  2ndmbfm  34228  eulerpartlemd  34333  oddprm2  34622  lfuhgr  35090  cvmlift2lem12  35286  bj-rest10  37061  topdifinfeq  37323  finxpsuclem  37370  curunc  37581  istotbnd2  37749  sstotbnd2  37753  isbnd3b  37764  totbndbnd  37768  br1cnvres  38243  fimgmcyc  42507  islnr2  43087  areaquad  43189  tfsconcat0i  43318  afv2res  47224  oddm1evenALTV  47660  oddp1evenALTV  47661  iscnrm3v  48938  isprsd  48940  joindm2  48953  meetdm2  48955  postcposALT  49554  postc  49555