Theorem baibd 541

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 530	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 222	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 511	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

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

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 398

This theorem is referenced by:  rbaibd  542  pw2f1olem  9076  eluz  12836  elicc4  13391  s111  14565  limsupgle  15421  lo1resb  15508  o1resb  15510  isercolllem2  15612  divalgmodcl  16350  ismri2  17576  acsfiel2  17599  eqglact  19059  eqgid  19060  cntzel  19187  dprdsubg  19894  subgdmdprd  19904  dprd2da  19912  dmdprdpr  19919  issubrg3  20347  ishil2  21274  obslbs  21285  iscld2  22532  isperf3  22657  cncnp2  22785  cnnei  22786  trfbas2  23347  flimrest  23487  flfnei  23495  fclsrest  23528  tsmssubm  23647  isnghm2  24241  isnghm3  24242  isnmhm2  24269  iscfil2  24783  caucfil  24800  ellimc2  25394  cnlimc  25405  lhop1  25531  dvfsumlem1  25543  fsumharmonic  26516  fsumvma  26716  fsumvma2  26717  vmasum  26719  chpchtsum  26722  chpub  26723  rpvmasum2  27015  dchrisum0lem1  27019  dirith  27032  uvtx2vtx1edg  28655  uvtx2vtx1edgb  28656  iscplgrnb  28673  frgr3v  29528  adjeu  31142  suppiniseg  31908  suppss3  31949  nndiffz1  31997  islinds5  32480  fsumcvg4  32930  qqhval2lem  32961  indpreima  33023  eulerpartlemf  33369  elorvc  33458  hashreprin  33632  neibastop3  35247  relowlpssretop  36245  sstotbnd2  36642  isbnd3b  36653  lshpkr  37987  isat2  38157  islln4  38378  islpln4  38402  islvol4  38445  islhp2  38868  pw2f1o2val2  41779  rfcnpre1  43703  rfcnpre2  43715  joindm3  47602  meetdm3  47604  catprsc  47633