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  8832  eluz  12578  elicc4  13128  s111  14301  limsupgle  15167  lo1resb  15254  o1resb  15256  isercolllem2  15358  divalgmodcl  16097  ismri2  17322  acsfiel2  17345  eqglact  18788  eqgid  18789  cntzel  18910  dprdsubg  19608  subgdmdprd  19618  dprd2da  19626  dmdprdpr  19633  issubrg3  20033  ishil2  20907  obslbs  20918  iscld2  22160  isperf3  22285  cncnp2  22413  cnnei  22414  trfbas2  22975  flimrest  23115  flfnei  23123  fclsrest  23156  tsmssubm  23275  isnghm2  23869  isnghm3  23870  isnmhm2  23897  iscfil2  24411  caucfil  24428  ellimc2  25022  cnlimc  25033  lhop1  25159  dvfsumlem1  25171  fsumharmonic  26142  fsumvma  26342  fsumvma2  26343  vmasum  26345  chpchtsum  26348  chpub  26349  rpvmasum2  26641  dchrisum0lem1  26645  dirith  26658  uvtx2vtx1edg  27746  uvtx2vtx1edgb  27747  iscplgrnb  27764  frgr3v  28618  adjeu  30230  suppiniseg  30999  suppss3  31038  nndiffz1  31086  islinds5  31542  fsumcvg4  31879  qqhval2lem  31910  indpreima  31972  eulerpartlemf  32316  elorvc  32405  hashreprin  32579  neibastop3  34530  relowlpssretop  35514  sstotbnd2  35911  isbnd3b  35922  lshpkr  37110  isat2  37280  islln4  37500  islpln4  37524  islvol4  37567  islhp2  37990  pw2f1o2val2  40842  rfcnpre1  42515  rfcnpre2  42527  joindm3  46215  meetdm3  46217  catprsc  46246