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  3635  elrab3  3672  dfpss3  4064  rabsn  4697  elrint2  4966  opres  5976  cores  6238  fnres  6664  fvres  6894  fvmpti  6984  f1ompt  7100  fliftfun  7304  isocnv3  7324  riotaxfrd  7394  ovid  7546  nlimon  7844  limom  7875  brdifun  8747  xpcomco  9074  0sdomg  9116  0sdomgOLD  9117  f1finf1o  9275  f1finf1oOLD  9276  ordtypelem9  9538  isacn  10056  alephinit  10107  isfin5-2  10403  pwfseqlem1  10670  pwfseqlem3  10672  pwfseqlem4  10674  ltresr  11152  xrlenlt  11298  znnnlt1  12617  difrp  13045  elfz  13528  fzolb2  13681  elfzo3  13691  fzouzsplit  13709  rabssnn0fi  14002  caubnd  15375  ello12  15530  elo12  15541  bitsval2  16442  smueqlem  16507  rpexp  16739  ramcl  17047  ismon2  17745  isepi2  17752  isfull2  17924  isfth2  17928  isghm3  19198  gastacos  19291  sylow2alem2  19597  lssnle  19653  isabl2  19769  submcmn2  19818  iscyggen2  19860  iscyg3  19865  cyggexb  19878  gsum2d2  19953  dprdw  19991  dprd2da  20023  iscrng2  20210  dvdsr2  20321  dfrhm2  20432  isdomn2  20669  isdomn2OLD  20670  sdrgacs  20759  islmhm3  20984  prmirredlem  21431  chrnzr  21489  iunocv  21639  iscss2  21644  ishil2  21677  obselocv  21686  psrbaglefi  21884  mplsubrglem  21962  bastop1  22929  isclo  23023  maxlp  23083  isperf2  23088  restperf  23120  cnpnei  23200  cnntr  23211  cnprest  23225  cnprest2  23226  lmres  23236  iscnrm2  23274  ist0-2  23280  ist1-2  23283  ishaus2  23287  tgcmp  23337  cmpfi  23344  dfconn2  23355  t1connperf  23372  subislly  23417  tx1cn  23545  tx2cn  23546  xkopt  23591  xkoinjcn  23623  ist0-4  23665  trfil2  23823  fin1aufil  23868  flimtopon  23906  elflim  23907  fclstopon  23948  isfcls2  23949  alexsubALTlem4  23986  ptcmplem3  23990  tgphaus  24053  xmetec  24371  prdsbl  24428  blval2  24499  isnvc2  24636  isnghm2  24661  isnmhm2  24689  0nmhm  24692  xrtgioo  24744  cncfcnvcn  24868  evth  24907  nmhmcn  25069  cmsss  25301  lssbn  25302  srabn  25310  ishl2  25320  ivthlem2  25403  0plef  25623  itg2monolem1  25701  itg2cnlem1  25712  itg2cnlem2  25713  ellimc2  25828  dvne0  25966  ellogdm  26598  dcubic  26806  atans2  26891  amgm  26951  ftalem3  27035  pclogsum  27176  dchrelbas3  27199  lgsabs1  27297  dchrvmaeq0  27465  rpvmasum2  27473  tgjustf  28398  clwwlkwwlksb  29981  ajval  30788  bnsscmcl  30795  axhcompl-zf  30925  seq1hcau  31114  hlim2  31119  issh3  31146  lnopcnre  31966  dmdbr2  32230  elatcv0  32268  iunsnima  32544  iunsnima2  32545  ecxpid  33322  ssdifidlprm  33419  ist0cld  33810  1stmbfm  34238  2ndmbfm  34239  eulerpartlemd  34344  oddprm2  34633  lfuhgr  35086  cvmlift2lem12  35282  bj-rest10  37052  topdifinfeq  37314  finxpsuclem  37361  curunc  37572  istotbnd2  37740  sstotbnd2  37744  isbnd3b  37755  totbndbnd  37759  br1cnvres  38233  ecres2  38243  fimgmcyc  42504  islnr2  43085  areaquad  43187  tfsconcat0i  43316  afv2res  47216  oddm1evenALTV  47637  oddp1evenALTV  47638  iscnrm3v  48875  isprsd  48877  joindm2  48890  meetdm2  48892  postcposALT  49393  postc  49394