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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  rbaibd  540  pw2f1olem  9072  eluz  12833  elicc4  13388  s111  14562  limsupgle  15418  lo1resb  15505  o1resb  15507  isercolllem2  15609  divalgmodcl  16347  ismri2  17575  acsfiel2  17598  eqglact  19096  eqgid  19097  cntzel  19229  dprdsubg  19936  subgdmdprd  19946  dprd2da  19954  dmdprdpr  19961  issubrg3  20492  ishil2  21582  obslbs  21593  iscld2  22854  isperf3  22979  cncnp2  23107  cnnei  23108  trfbas2  23669  flimrest  23809  flfnei  23817  fclsrest  23850  tsmssubm  23969  isnghm2  24563  isnghm3  24564  isnmhm2  24591  iscfil2  25116  caucfil  25133  ellimc2  25728  cnlimc  25739  lhop1  25869  dvfsumlem1  25882  fsumharmonic  26860  fsumvma  27062  fsumvma2  27063  vmasum  27065  chpchtsum  27068  chpub  27069  rpvmasum2  27361  dchrisum0lem1  27365  dirith  27378  uvtx2vtx1edg  29124  uvtx2vtx1edgb  29125  iscplgrnb  29142  frgr3v  29997  adjeu  31611  suppiniseg  32377  suppss3  32418  nndiffz1  32466  islinds5  32949  fsumcvg4  33419  qqhval2lem  33450  indpreima  33512  eulerpartlemf  33858  elorvc  33947  hashreprin  34121  neibastop3  35737  relowlpssretop  36735  sstotbnd2  37132  isbnd3b  37143  lshpkr  38477  isat2  38647  islln4  38868  islpln4  38892  islvol4  38935  islhp2  39358  pw2f1o2val2  42268  rfcnpre1  44192  rfcnpre2  44204  joindm3  47790  meetdm3  47792  catprsc  47821