Theorem baib 536

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  baibr  537  ceqsrexbv  3643  elrab3  3683  dfpss3  4085  rabsn  4724  elrint2  4995  opres  5989  cores  6245  fnres  6674  fvres  6907  fvmpti  6994  f1ompt  7107  fliftfun  7305  isocnv3  7325  riotaxfrd  7396  ovid  7545  nlimon  7836  limom  7867  brdifun  8728  xpcomco  9058  0sdomg  9100  0sdomgOLD  9101  f1finf1o  9267  f1finf1oOLD  9268  ordtypelem9  9517  isacn  10035  alephinit  10086  isfin5-2  10382  pwfseqlem1  10649  pwfseqlem3  10651  pwfseqlem4  10653  ltresr  11131  xrlenlt  11275  znnnlt1  12585  difrp  13008  elfz  13486  fzolb2  13635  elfzo3  13645  fzouzsplit  13663  rabssnn0fi  13947  caubnd  15301  ello12  15456  elo12  15467  bitsval2  16362  smueqlem  16427  rpexp  16655  ramcl  16958  ismon2  17677  isepi2  17684  isfull2  17858  isfth2  17862  isghm3  19087  gastacos  19168  sylow2alem2  19480  lssnle  19536  isabl2  19652  submcmn2  19701  iscyggen2  19743  iscyg3  19748  cyggexb  19761  gsum2d2  19836  dprdw  19874  dprd2da  19906  iscrng2  20068  dvdsr2  20169  dfrhm2  20245  sdrgacs  20409  islmhm3  20631  isdomn2  20907  prmirredlem  21033  chrnzr  21073  iunocv  21225  iscss2  21230  ishil2  21265  obselocv  21274  psrbaglefi  21476  psrbaglefiOLD  21477  mplsubrglem  21554  bastop1  22487  isclo  22582  maxlp  22642  isperf2  22647  restperf  22679  cnpnei  22759  cnntr  22770  cnprest  22784  cnprest2  22785  lmres  22795  iscnrm2  22833  ist0-2  22839  ist1-2  22842  ishaus2  22846  tgcmp  22896  cmpfi  22903  dfconn2  22914  t1connperf  22931  subislly  22976  tx1cn  23104  tx2cn  23105  xkopt  23150  xkoinjcn  23182  ist0-4  23224  trfil2  23382  fin1aufil  23427  flimtopon  23465  elflim  23466  fclstopon  23507  isfcls2  23508  alexsubALTlem4  23545  ptcmplem3  23549  tgphaus  23612  xmetec  23931  prdsbl  23991  blval2  24062  isnvc2  24207  isnghm2  24232  isnmhm2  24260  0nmhm  24263  xrtgioo  24313  cncfcnvcn  24432  evth  24466  nmhmcn  24627  cmsss  24859  lssbn  24860  srabn  24868  ishl2  24878  ivthlem2  24960  0plef  25180  itg2monolem1  25259  itg2cnlem1  25270  itg2cnlem2  25271  ellimc2  25385  dvne0  25519  ellogdm  26138  dcubic  26340  atans2  26425  amgm  26484  ftalem3  26568  pclogsum  26707  dchrelbas3  26730  lgsabs1  26828  dchrvmaeq0  26996  rpvmasum2  27004  tgjustf  27713  clwwlkwwlksb  29296  ajval  30101  bnsscmcl  30108  axhcompl-zf  30238  seq1hcau  30427  hlim2  30432  issh3  30459  lnopcnre  31279  dmdbr2  31543  elatcv0  31581  iunsnima  31834  iunsnima2  31835  ecxpid  32460  ist0cld  32801  1stmbfm  33247  2ndmbfm  33248  eulerpartlemd  33353  oddprm2  33655  lfuhgr  34096  cvmlift2lem12  34293  bj-rest10  35957  topdifinfeq  36219  finxpsuclem  36266  curunc  36458  istotbnd2  36626  sstotbnd2  36630  isbnd3b  36641  totbndbnd  36645  br1cnvres  37125  ecres2  37135  islnr2  41841  areaquad  41950  tfsconcat0i  42080  afv2res  45933  oddm1evenALTV  46329  oddp1evenALTV  46330  iscnrm3v  47539  isprsd  47541  joindm2  47554  meetdm2  47556  postcposALT  47654  postc  47655