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  3669  elrab3  3709  dfpss3  4112  rabsn  4746  elrint2  5014  opres  6019  cores  6280  fnres  6707  fvres  6939  fvmpti  7028  f1ompt  7145  fliftfun  7348  isocnv3  7368  riotaxfrd  7439  ovid  7591  nlimon  7888  limom  7919  brdifun  8793  xpcomco  9128  0sdomg  9170  0sdomgOLD  9171  f1finf1o  9333  f1finf1oOLD  9334  ordtypelem9  9595  isacn  10113  alephinit  10164  isfin5-2  10460  pwfseqlem1  10727  pwfseqlem3  10729  pwfseqlem4  10731  ltresr  11209  xrlenlt  11355  znnnlt1  12670  difrp  13095  elfz  13573  fzolb2  13723  elfzo3  13733  fzouzsplit  13751  rabssnn0fi  14037  caubnd  15407  ello12  15562  elo12  15573  bitsval2  16471  smueqlem  16536  rpexp  16769  ramcl  17076  ismon2  17795  isepi2  17802  isfull2  17978  isfth2  17982  isghm3  19257  gastacos  19350  sylow2alem2  19660  lssnle  19716  isabl2  19832  submcmn2  19881  iscyggen2  19923  iscyg3  19928  cyggexb  19941  gsum2d2  20016  dprdw  20054  dprd2da  20086  iscrng2  20279  dvdsr2  20389  dfrhm2  20500  isdomn2  20733  isdomn2OLD  20734  sdrgacs  20824  islmhm3  21050  prmirredlem  21506  chrnzr  21568  iunocv  21722  iscss2  21727  ishil2  21762  obselocv  21771  psrbaglefi  21969  mplsubrglem  22047  bastop1  23021  isclo  23116  maxlp  23176  isperf2  23181  restperf  23213  cnpnei  23293  cnntr  23304  cnprest  23318  cnprest2  23319  lmres  23329  iscnrm2  23367  ist0-2  23373  ist1-2  23376  ishaus2  23380  tgcmp  23430  cmpfi  23437  dfconn2  23448  t1connperf  23465  subislly  23510  tx1cn  23638  tx2cn  23639  xkopt  23684  xkoinjcn  23716  ist0-4  23758  trfil2  23916  fin1aufil  23961  flimtopon  23999  elflim  24000  fclstopon  24041  isfcls2  24042  alexsubALTlem4  24079  ptcmplem3  24083  tgphaus  24146  xmetec  24465  prdsbl  24525  blval2  24596  isnvc2  24741  isnghm2  24766  isnmhm2  24794  0nmhm  24797  xrtgioo  24847  cncfcnvcn  24971  evth  25010  nmhmcn  25172  cmsss  25404  lssbn  25405  srabn  25413  ishl2  25423  ivthlem2  25506  0plef  25726  itg2monolem1  25805  itg2cnlem1  25816  itg2cnlem2  25817  ellimc2  25932  dvne0  26070  ellogdm  26699  dcubic  26907  atans2  26992  amgm  27052  ftalem3  27136  pclogsum  27277  dchrelbas3  27300  lgsabs1  27398  dchrvmaeq0  27566  rpvmasum2  27574  tgjustf  28499  clwwlkwwlksb  30086  ajval  30893  bnsscmcl  30900  axhcompl-zf  31030  seq1hcau  31219  hlim2  31224  issh3  31251  lnopcnre  32071  dmdbr2  32335  elatcv0  32373  iunsnima  32640  iunsnima2  32641  ecxpid  33354  ssdifidlprm  33451  ist0cld  33779  1stmbfm  34225  2ndmbfm  34226  eulerpartlemd  34331  oddprm2  34632  lfuhgr  35085  cvmlift2lem12  35282  bj-rest10  37054  topdifinfeq  37316  finxpsuclem  37363  curunc  37562  istotbnd2  37730  sstotbnd2  37734  isbnd3b  37745  totbndbnd  37749  br1cnvres  38225  ecres2  38235  fimgmcyc  42489  islnr2  43071  areaquad  43177  tfsconcat0i  43307  afv2res  47154  oddm1evenALTV  47549  oddp1evenALTV  47550  iscnrm3v  48633  isprsd  48635  joindm2  48648  meetdm2  48650  postcposALT  48748  postc  48749