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 290	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  3586  elrab3  3625  dfpss3  4021  rabsn  4657  elrint2  4923  opres  5901  cores  6153  fnres  6559  fvres  6793  fvmpti  6874  f1ompt  6985  fliftfun  7183  isocnv3  7203  riotaxfrd  7267  ovid  7414  nlimon  7698  limom  7728  brdifun  8527  xpcomco  8849  0sdomg  8891  0sdomgOLD  8892  f1finf1o  9046  ordtypelem9  9285  isacn  9800  alephinit  9851  isfin5-2  10147  pwfseqlem1  10414  pwfseqlem3  10416  pwfseqlem4  10418  ltresr  10896  xrlenlt  11040  znnnlt1  12347  difrp  12768  elfz  13245  fzolb2  13394  elfzo3  13404  fzouzsplit  13422  rabssnn0fi  13706  caubnd  15070  ello12  15225  elo12  15236  bitsval2  16132  smueqlem  16197  rpexp  16427  ramcl  16730  ismon2  17446  isepi2  17453  isfull2  17627  isfth2  17631  isghm3  18835  gastacos  18916  sylow2alem2  19223  lssnle  19280  isabl2  19395  submcmn2  19440  iscyggen2  19481  iscyg3  19486  cyggexb  19500  gsum2d2  19575  dprdw  19613  dprd2da  19645  iscrng2  19802  dvdsr2  19889  dfrhm2  19961  sdrgacs  20069  islmhm3  20290  isdomn2  20570  prmirredlem  20694  chrnzr  20734  iunocv  20886  iscss2  20891  ishil2  20926  obselocv  20935  psrbaglefi  21135  psrbaglefiOLD  21136  mplsubrglem  21210  bastop1  22143  isclo  22238  maxlp  22298  isperf2  22303  restperf  22335  cnpnei  22415  cnntr  22426  cnprest  22440  cnprest2  22441  lmres  22451  iscnrm2  22489  ist0-2  22495  ist1-2  22498  ishaus2  22502  tgcmp  22552  cmpfi  22559  dfconn2  22570  t1connperf  22587  subislly  22632  tx1cn  22760  tx2cn  22761  xkopt  22806  xkoinjcn  22838  ist0-4  22880  trfil2  23038  fin1aufil  23083  flimtopon  23121  elflim  23122  fclstopon  23163  isfcls2  23164  alexsubALTlem4  23201  ptcmplem3  23205  tgphaus  23268  xmetec  23587  prdsbl  23647  blval2  23718  isnvc2  23863  isnghm2  23888  isnmhm2  23916  0nmhm  23919  xrtgioo  23969  cncfcnvcn  24088  evth  24122  nmhmcn  24283  cmsss  24515  lssbn  24516  srabn  24524  ishl2  24534  ivthlem2  24616  0plef  24836  itg2monolem1  24915  itg2cnlem1  24926  itg2cnlem2  24927  ellimc2  25041  dvne0  25175  ellogdm  25794  dcubic  25996  atans2  26081  amgm  26140  ftalem3  26224  pclogsum  26363  dchrelbas3  26386  lgsabs1  26484  dchrvmaeq0  26652  rpvmasum2  26660  tgjustf  26834  clwwlkwwlksb  28418  ajval  29223  bnsscmcl  29230  axhcompl-zf  29360  seq1hcau  29549  hlim2  29554  issh3  29581  lnopcnre  30401  dmdbr2  30665  elatcv0  30703  iunsnima  30958  iunsnima2  30959  ecxpid  31556  ist0cld  31783  1stmbfm  32227  2ndmbfm  32228  eulerpartlemd  32333  oddprm2  32635  lfuhgr  33079  cvmlift2lem12  33276  bj-rest10  35259  topdifinfeq  35521  finxpsuclem  35568  curunc  35759  istotbnd2  35928  sstotbnd2  35932  isbnd3b  35943  totbndbnd  35947  ecres2  36414  islnr2  40939  areaquad  41047  afv2res  44731  oddm1evenALTV  45127  oddp1evenALTV  45128  iscnrm3v  46247  isprsd  46249  joindm2  46262  meetdm2  46264  postcposALT  46362  postc  46363