Theorem baib 942

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		ibar 524	. 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
2		baib.1	. 2 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
3	1, 2	syl6rbbr 278	1 ⊢ (𝜓 → (𝜑 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  baibr  943  ceqsrexbv  3307  elrab3  3332  dfpss3  3655  rabsn  4200  elrint2  4454  elpredg  5611  fnres  5921  fvmpti  6190  f1ompt  6290  fliftfun  6462  isocnv3  6482  riotaxfrd  6541  ovid  6675  nlimon  6943  limom  6972  brdifun  7658  xpcomco  7935  0sdomg  7974  f1finf1o  8072  ordtypelem9  8314  isacn  8750  alephinit  8801  isfin5-2  9096  pwfseqlem1  9359  pwfseqlem3  9361  pwfseqlem4  9363  ltresr  9840  xrlenlt  9982  znnnlt1  11281  difrp  11744  elfz  12203  fzolb2  12346  elfzo3  12355  fzouzsplit  12372  rabssnn0fi  12647  caubnd  13946  ello12  14095  elo12  14106  bitsval2  14985  smueqlem  15050  rpexp  15270  ramcl  15571  ismon2  16217  isepi2  16224  isfull2  16394  isfth2  16398  isghm3  17484  gastacos  17566  sylow2alem2  17856  lssnle  17910  isabl2  18024  submcmn2  18067  iscyggen2  18106  iscyg3  18111  cyggexb  18123  gsum2d2  18196  dprdw  18232  dprd2da  18264  iscrng2  18386  dvdsr2  18470  dfrhm2  18540  islmhm3  18849  isdomn2  19120  psrbaglefi  19193  mplsubrglem  19260  prmirredlem  19660  chrnzr  19697  iunocv  19844  iscss2  19849  ishil2  19882  obselocv  19891  bastop1  20608  isclo  20701  maxlp  20761  isperf2  20766  restperf  20798  cnpnei  20878  cnntr  20889  cnprest  20903  cnprest2  20904  lmres  20914  iscnrm2  20952  ist0-2  20958  ist1-2  20961  ishaus2  20965  tgcmp  21014  cmpfi  21021  dfcon2  21032  t1conperf  21049  subislly  21094  tx1cn  21222  tx2cn  21223  xkopt  21268  xkoinjcn  21300  ist0-4  21342  trfil2  21501  fin1aufil  21546  flimtopon  21584  elflim  21585  fclstopon  21626  isfcls2  21627  alexsubALTlem4  21664  ptcmplem3  21668  tgphaus  21730  xmetec  22049  prdsbl  22106  blval2  22177  isnvc2  22313  isnghm2  22338  isnmhm2  22366  0nmhm  22369  xrtgioo  22417  cncfcnvcn  22532  evth  22566  nmhmcn  22728  cmsss  22955  lssbn  22956  srabn  22964  ishl2  22974  ivthlem2  23028  0plef  23245  itg2monolem1  23323  itg2cnlem1  23334  itg2cnlem2  23335  ellimc2  23447  dvne0  23578  ellogdm  24185  dcubic  24373  atans2  24458  amgm  24517  ftalem3  24601  pclogsum  24740  dchrelbas3  24763  lgsabs1  24861  dchrvmaeq0  24993  rpvmasum2  25001  ajval  27101  bnsscmcl  27108  axhcompl-zf  27239  seq1hcau  27428  hlim2  27433  issh3  27460  lnopcnre  28282  dmdbr2  28546  elatcv0  28584  iunsnima  28808  1stmbfm  29649  2ndmbfm  29650  eulerpartlemd  29755  cvmlift2lem12  30550  bj-rest10  32222  topdifinfeq  32374  finxpsuclem  32410  curunc  32561  istotbnd2  32739  sstotbnd2  32743  isbnd3b  32754  totbndbnd  32758  islnr2  36703  sdrgacs  36790  areaquad  36821  oddm1evenALTV  40124  oddp1evenALTV  40125