Theorem baibd 539

Description: Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypothesis

Ref	Expression
baibd.1	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
baibd	⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Proof of Theorem baibd

Step	Hyp	Ref	Expression
1		baibd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2		ibar 528	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 223	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 509	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:  rbaibd  540  bian1d  580  pw2f1olem  9021  eluz  12777  elicc4  13341  s111  14551  limsupgle  15412  lo1resb  15499  o1resb  15501  isercolllem2  15601  divalgmodcl  16346  ismri2  17567  acsfiel2  17590  eqglact  19120  eqgid  19121  cntzel  19264  dprdsubg  19967  subgdmdprd  19977  dprd2da  19985  dmdprdpr  19992  issubrg3  20545  ishil2  21686  obslbs  21697  iscld2  22984  isperf3  23109  cncnp2  23237  cnnei  23238  trfbas2  23799  flimrest  23939  flfnei  23947  fclsrest  23980  tsmssubm  24099  isnghm2  24680  isnghm3  24681  isnmhm2  24708  iscfil2  25234  caucfil  25251  ellimc2  25846  cnlimc  25857  lhop1  25987  dvfsumlem1  26000  fsumharmonic  26990  fsumvma  27192  fsumvma2  27193  vmasum  27195  chpchtsum  27198  chpub  27199  rpvmasum2  27491  dchrisum0lem1  27495  dirith  27508  uvtx2vtx1edg  29483  uvtx2vtx1edgb  29484  iscplgrnb  29501  frgr3v  30362  adjeu  31977  suppiniseg  32776  suppss3  32813  nndiffz1  32877  indpreima  32958  islinds5  33460  fsumcvg4  34128  qqhval2lem  34159  eulerpartlemf  34548  elorvc  34638  hashreprin  34798  neibastop3  36578  relowlpssretop  37619  sstotbnd2  38025  isbnd3b  38036  lshpkr  39493  isat2  39663  islln4  39883  islpln4  39907  islvol4  39950  islhp2  40373  pw2f1o2val2  43397  modelaxreplem3  45336  rfcnpre1  45379  rfcnpre2  45391  joindm3  49328  meetdm3  49330  catprsc  49372