Theorem baibd 543

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  rbaibd  544  pw2f1olem  8604  eluz  12245  elicc4  12792  s111  13960  limsupgle  14826  lo1resb  14913  o1resb  14915  isercolllem2  15014  divalgmodcl  15748  ismri2  16895  acsfiel2  16918  eqglact  18323  eqgid  18324  cntzel  18445  dprdsubg  19139  subgdmdprd  19149  dprd2da  19157  dmdprdpr  19164  issubrg3  19556  ishil2  20408  obslbs  20419  iscld2  21633  isperf3  21758  cncnp2  21886  cnnei  21887  trfbas2  22448  flimrest  22588  flfnei  22596  fclsrest  22629  tsmssubm  22748  isnghm2  23330  isnghm3  23331  isnmhm2  23358  iscfil2  23870  caucfil  23887  ellimc2  24480  cnlimc  24491  lhop1  24617  dvfsumlem1  24629  fsumharmonic  25597  fsumvma  25797  fsumvma2  25798  vmasum  25800  chpchtsum  25803  chpub  25804  rpvmasum2  26096  dchrisum0lem1  26100  dirith  26113  uvtx2vtx1edg  27188  uvtx2vtx1edgb  27189  iscplgrnb  27206  frgr3v  28060  adjeu  29672  suppiniseg  30446  suppss3  30486  nndiffz1  30535  islinds5  30983  fsumcvg4  31303  qqhval2lem  31332  indpreima  31394  eulerpartlemf  31738  elorvc  31827  hashreprin  32001  neibastop3  33823  relowlpssretop  34781  sstotbnd2  35212  isbnd3b  35223  lshpkr  36413  isat2  36583  islln4  36803  islpln4  36827  islvol4  36870  islhp2  37293  pw2f1o2val2  39981  rfcnpre1  41648  rfcnpre2  41660