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  9092  eluz  12858  elicc4  13415  s111  14589  limsupgle  15445  lo1resb  15532  o1resb  15534  isercolllem2  15636  divalgmodcl  16375  ismri2  17603  acsfiel2  17626  eqglact  19125  eqgid  19126  cntzel  19265  dprdsubg  19972  subgdmdprd  19982  dprd2da  19990  dmdprdpr  19997  issubrg3  20528  ishil2  21640  obslbs  21651  iscld2  22919  isperf3  23044  cncnp2  23172  cnnei  23173  trfbas2  23734  flimrest  23874  flfnei  23882  fclsrest  23915  tsmssubm  24034  isnghm2  24628  isnghm3  24629  isnmhm2  24656  iscfil2  25181  caucfil  25198  ellimc2  25793  cnlimc  25804  lhop1  25934  dvfsumlem1  25947  fsumharmonic  26931  fsumvma  27133  fsumvma2  27134  vmasum  27136  chpchtsum  27139  chpub  27140  rpvmasum2  27432  dchrisum0lem1  27436  dirith  27449  uvtx2vtx1edg  29198  uvtx2vtx1edgb  29199  iscplgrnb  29216  frgr3v  30072  adjeu  31686  suppiniseg  32450  suppss3  32490  nndiffz1  32538  islinds5  33019  fsumcvg4  33487  qqhval2lem  33518  indpreima  33580  eulerpartlemf  33926  elorvc  34015  hashreprin  34188  neibastop3  35782  relowlpssretop  36779  sstotbnd2  37182  isbnd3b  37193  lshpkr  38526  isat2  38696  islln4  38917  islpln4  38941  islvol4  38984  islhp2  39407  pw2f1o2val2  42383  rfcnpre1  44304  rfcnpre2  44316  joindm3  47911  meetdm3  47913  catprsc  47942