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  pw2f1olem  9050  eluz  12814  elicc4  13381  s111  14587  limsupgle  15450  lo1resb  15537  o1resb  15539  isercolllem2  15639  divalgmodcl  16384  ismri2  17600  acsfiel2  17623  eqglact  19118  eqgid  19119  cntzel  19262  dprdsubg  19963  subgdmdprd  19973  dprd2da  19981  dmdprdpr  19988  issubrg3  20516  ishil2  21635  obslbs  21646  iscld2  22922  isperf3  23047  cncnp2  23175  cnnei  23176  trfbas2  23737  flimrest  23877  flfnei  23885  fclsrest  23918  tsmssubm  24037  isnghm2  24619  isnghm3  24620  isnmhm2  24647  iscfil2  25173  caucfil  25190  ellimc2  25785  cnlimc  25796  lhop1  25926  dvfsumlem1  25939  fsumharmonic  26929  fsumvma  27131  fsumvma2  27132  vmasum  27134  chpchtsum  27137  chpub  27138  rpvmasum2  27430  dchrisum0lem1  27434  dirith  27447  uvtx2vtx1edg  29332  uvtx2vtx1edgb  29333  iscplgrnb  29350  frgr3v  30211  adjeu  31825  suppiniseg  32616  suppss3  32654  nndiffz1  32716  indpreima  32795  islinds5  33345  fsumcvg4  33947  qqhval2lem  33978  eulerpartlemf  34368  elorvc  34458  hashreprin  34618  neibastop3  36357  relowlpssretop  37359  sstotbnd2  37775  isbnd3b  37786  lshpkr  39117  isat2  39287  islln4  39508  islpln4  39532  islvol4  39575  islhp2  39998  pw2f1o2val2  43036  modelaxreplem3  44977  rfcnpre1  45020  rfcnpre2  45032  joindm3  48961  meetdm3  48963  catprsc  49006