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  3625  elrab3  3663  dfpss3  4055  rabsn  4688  elrint2  4957  opres  5963  cores  6225  fnres  6648  fvres  6880  fvmpti  6970  f1ompt  7086  fliftfun  7290  isocnv3  7310  riotaxfrd  7381  ovid  7533  nlimon  7830  limom  7861  brdifun  8704  elecreseq  8723  xpcomco  9036  0sdomg  9076  f1finf1o  9223  f1finf1oOLD  9224  ordtypelem9  9486  isacn  10004  alephinit  10055  isfin5-2  10351  pwfseqlem1  10618  pwfseqlem3  10620  pwfseqlem4  10622  ltresr  11100  xrlenlt  11246  znnnlt1  12567  difrp  12998  elfz  13481  fzolb2  13634  elfzo3  13644  fzouzsplit  13662  rabssnn0fi  13958  caubnd  15332  ello12  15489  elo12  15500  bitsval2  16402  smueqlem  16467  rpexp  16699  ramcl  17007  ismon2  17703  isepi2  17710  isfull2  17882  isfth2  17886  isghm3  19156  gastacos  19249  sylow2alem2  19555  lssnle  19611  isabl2  19727  submcmn2  19776  iscyggen2  19818  iscyg3  19823  cyggexb  19836  gsum2d2  19911  dprdw  19949  dprd2da  19981  iscrng2  20168  dvdsr2  20279  dfrhm2  20390  isdomn2  20627  isdomn2OLD  20628  sdrgacs  20717  islmhm3  20942  prmirredlem  21389  chrnzr  21447  iunocv  21597  iscss2  21602  ishil2  21635  obselocv  21644  psrbaglefi  21842  mplsubrglem  21920  bastop1  22887  isclo  22981  maxlp  23041  isperf2  23046  restperf  23078  cnpnei  23158  cnntr  23169  cnprest  23183  cnprest2  23184  lmres  23194  iscnrm2  23232  ist0-2  23238  ist1-2  23241  ishaus2  23245  tgcmp  23295  cmpfi  23302  dfconn2  23313  t1connperf  23330  subislly  23375  tx1cn  23503  tx2cn  23504  xkopt  23549  xkoinjcn  23581  ist0-4  23623  trfil2  23781  fin1aufil  23826  flimtopon  23864  elflim  23865  fclstopon  23906  isfcls2  23907  alexsubALTlem4  23944  ptcmplem3  23948  tgphaus  24011  xmetec  24329  prdsbl  24386  blval2  24457  isnvc2  24594  isnghm2  24619  isnmhm2  24647  0nmhm  24650  xrtgioo  24702  cncfcnvcn  24826  evth  24865  nmhmcn  25027  cmsss  25258  lssbn  25259  srabn  25267  ishl2  25277  ivthlem2  25360  0plef  25580  itg2monolem1  25658  itg2cnlem1  25669  itg2cnlem2  25670  ellimc2  25785  dvne0  25923  ellogdm  26555  dcubic  26763  atans2  26848  amgm  26908  ftalem3  26992  pclogsum  27133  dchrelbas3  27156  lgsabs1  27254  dchrvmaeq0  27422  rpvmasum2  27430  tgjustf  28407  clwwlkwwlksb  29990  ajval  30797  bnsscmcl  30804  axhcompl-zf  30934  seq1hcau  31123  hlim2  31128  issh3  31155  lnopcnre  31975  dmdbr2  32239  elatcv0  32277  iunsnima  32553  iunsnima2  32554  ecxpid  33339  ssdifidlprm  33436  ist0cld  33830  1stmbfm  34258  2ndmbfm  34259  eulerpartlemd  34364  oddprm2  34653  lfuhgr  35112  cvmlift2lem12  35308  bj-rest10  37083  topdifinfeq  37345  finxpsuclem  37392  curunc  37603  istotbnd2  37771  sstotbnd2  37775  isbnd3b  37786  totbndbnd  37790  br1cnvres  38265  fimgmcyc  42529  islnr2  43110  areaquad  43212  tfsconcat0i  43341  afv2res  47244  oddm1evenALTV  47680  oddp1evenALTV  47681  iscnrm3v  48945  isprsd  48947  joindm2  48960  meetdm2  48962  postcposALT  49561  postc  49562