Theorem baib 543

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  baibr  544  ceqsrexbv  3615  elrab3  3651  dfpss3  4042  rabsn  4679  elrint2  4947  opres  5973  cores  6232  fnres  6644  fvres  6882  fvmpti  6970  f1ompt  7088  fliftfun  7292  isocnv3  7312  riotaxfrd  7383  ovid  7533  nlimon  7827  limom  7858  brdifun  8704  elecreseq  8723  xpcomco  9035  0sdomg  9074  f1finf1o  9213  ordtypelem9  9471  isacn  9997  alephinit  10048  isfin5-2  10345  pwfseqlem1  10613  pwfseqlem3  10615  pwfseqlem4  10617  ltresr  11095  xrlenlt  11244  znnnlt1  12595  difrp  13030  elfz  13515  fzolb2  13669  elfzo3  13679  fzouzsplit  13697  rabssnn0fi  13996  caubnd  15369  ello12  15526  elo12  15537  bitsval2  16442  smueqlem  16507  rpexp  16740  ramcl  17048  ismon2  17750  isepi2  17757  isfull2  17929  isfth2  17933  isghm3  19240  gastacos  19333  sylow2alem2  19641  lssnle  19697  isabl2  19813  submcmn2  19862  iscyggen2  19904  iscyg3  19909  cyggexb  19922  gsum2d2  19997  dprdw  20035  dprd2da  20067  iscrng2  20281  dvdsr2  20391  dfrhm2  20502  isdomn2  20740  isdomn2OLD  20741  sdrgacs  20830  islmhm3  21075  prmirredlem  21504  chrnzr  21562  iunocv  21713  iscss2  21718  ishil2  21751  obselocv  21760  psrbaglefi  21958  mplsubrglem  22035  bastop1  23033  isclo  23127  maxlp  23187  isperf2  23192  restperf  23224  cnpnei  23304  cnntr  23315  cnprest  23329  cnprest2  23330  lmres  23340  iscnrm2  23378  ist0-2  23384  ist1-2  23387  ishaus2  23391  tgcmp  23441  cmpfi  23448  dfconn2  23459  t1connperf  23476  subislly  23521  tx1cn  23649  tx2cn  23650  xkopt  23695  xkoinjcn  23727  ist0-4  23769  trfil2  23927  fin1aufil  23972  flimtopon  24010  elflim  24011  fclstopon  24052  isfcls2  24053  alexsubALTlem4  24090  ptcmplem3  24094  tgphaus  24157  xmetec  24474  prdsbl  24531  blval2  24602  isnvc2  24739  isnghm2  24764  isnmhm2  24792  0nmhm  24795  xrtgioo  24847  cncfcnvcn  24967  evth  25001  nmhmcn  25162  cmsss  25393  lssbn  25394  srabn  25402  ishl2  25412  ivthlem2  25494  0plef  25714  itg2monolem1  25792  itg2cnlem1  25803  itg2cnlem2  25804  ellimc2  25919  dvne0  26053  ellogdm  26681  dcubic  26888  atans2  26973  amgm  27032  ftalem3  27116  pclogsum  27256  dchrelbas3  27279  lgsabs1  27377  dchrvmaeq0  27545  rpvmasum2  27553  tgjustf  28619  clwwlkwwlksb  30202  ajval  31010  bnsscmcl  31017  axhcompl-zf  31147  seq1hcau  31336  hlim2  31341  issh3  31368  lnopcnre  32188  dmdbr2  32452  elatcv0  32490  iunsnima  32770  iunsnima2  32771  partfun2  32828  ecxpid  33508  ssdifidlprm  33606  ist0cld  34091  1stmbfm  34518  2ndmbfm  34519  eulerpartlemd  34624  oddprm2  34913  lfuhgr  35432  cvmlift2lem12  35628  bj-rest10  37542  topdifinfeq  37808  finxpsuclem  37855  curunc  38065  istotbnd2  38233  sstotbnd2  38237  isbnd3b  38248  totbndbnd  38252  br1cnvres  38737  fimgmcyc  43116  islnr2  43655  areaquad  43757  tfsconcat0i  43886  afv2res  47797  oddm1evenALTV  48261  oddp1evenALTV  48262  iscnrm3v  49538  isprsd  49540  joindm2  49553  meetdm2  49555  postcposALT  50153  postc  50154