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 289	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  baibr  536  ceqsrexbv  3579  elrab3  3618  dfpss3  4017  rabsn  4654  elrint2  4920  opres  5890  cores  6142  fnres  6543  fvres  6775  fvmpti  6856  f1ompt  6967  fliftfun  7163  isocnv3  7183  riotaxfrd  7247  ovid  7392  nlimon  7673  limom  7703  brdifun  8485  xpcomco  8802  0sdomg  8842  f1finf1o  8975  ordtypelem9  9215  isacn  9731  alephinit  9782  isfin5-2  10078  pwfseqlem1  10345  pwfseqlem3  10347  pwfseqlem4  10349  ltresr  10827  xrlenlt  10971  znnnlt1  12277  difrp  12697  elfz  13174  fzolb2  13323  elfzo3  13332  fzouzsplit  13350  rabssnn0fi  13634  caubnd  14998  ello12  15153  elo12  15164  bitsval2  16060  smueqlem  16125  rpexp  16355  ramcl  16658  ismon2  17363  isepi2  17370  isfull2  17543  isfth2  17547  isghm3  18750  gastacos  18831  sylow2alem2  19138  lssnle  19195  isabl2  19310  submcmn2  19355  iscyggen2  19396  iscyg3  19401  cyggexb  19415  gsum2d2  19490  dprdw  19528  dprd2da  19560  iscrng2  19717  dvdsr2  19804  dfrhm2  19876  sdrgacs  19984  islmhm3  20205  isdomn2  20483  prmirredlem  20606  chrnzr  20646  iunocv  20798  iscss2  20803  ishil2  20836  obselocv  20845  psrbaglefi  21045  psrbaglefiOLD  21046  mplsubrglem  21120  bastop1  22051  isclo  22146  maxlp  22206  isperf2  22211  restperf  22243  cnpnei  22323  cnntr  22334  cnprest  22348  cnprest2  22349  lmres  22359  iscnrm2  22397  ist0-2  22403  ist1-2  22406  ishaus2  22410  tgcmp  22460  cmpfi  22467  dfconn2  22478  t1connperf  22495  subislly  22540  tx1cn  22668  tx2cn  22669  xkopt  22714  xkoinjcn  22746  ist0-4  22788  trfil2  22946  fin1aufil  22991  flimtopon  23029  elflim  23030  fclstopon  23071  isfcls2  23072  alexsubALTlem4  23109  ptcmplem3  23113  tgphaus  23176  xmetec  23495  prdsbl  23553  blval2  23624  isnvc2  23769  isnghm2  23794  isnmhm2  23822  0nmhm  23825  xrtgioo  23875  cncfcnvcn  23994  evth  24028  nmhmcn  24189  cmsss  24420  lssbn  24421  srabn  24429  ishl2  24439  ivthlem2  24521  0plef  24741  itg2monolem1  24820  itg2cnlem1  24831  itg2cnlem2  24832  ellimc2  24946  dvne0  25080  ellogdm  25699  dcubic  25901  atans2  25986  amgm  26045  ftalem3  26129  pclogsum  26268  dchrelbas3  26291  lgsabs1  26389  dchrvmaeq0  26557  rpvmasum2  26565  tgjustf  26738  clwwlkwwlksb  28319  ajval  29124  bnsscmcl  29131  axhcompl-zf  29261  seq1hcau  29450  hlim2  29455  issh3  29482  lnopcnre  30302  dmdbr2  30566  elatcv0  30604  iunsnima  30859  iunsnima2  30860  ecxpid  31458  ist0cld  31685  1stmbfm  32127  2ndmbfm  32128  eulerpartlemd  32233  oddprm2  32535  lfuhgr  32979  cvmlift2lem12  33176  bj-rest10  35186  topdifinfeq  35448  finxpsuclem  35495  curunc  35686  istotbnd2  35855  sstotbnd2  35859  isbnd3b  35870  totbndbnd  35874  ecres2  36341  islnr2  40855  areaquad  40963  afv2res  44618  oddm1evenALTV  45015  oddp1evenALTV  45016  iscnrm3v  46135  isprsd  46137  joindm2  46150  meetdm2  46152  postcposALT  46248  postc  46249