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  bian1d  580  pw2f1olem  9019  eluz  12802  elicc4  13366  s111  14578  limsupgle  15439  lo1resb  15526  o1resb  15528  isercolllem2  15628  divalgmodcl  16376  ismri2  17598  acsfiel2  17621  eqglact  19154  eqgid  19155  cntzel  19298  dprdsubg  20001  subgdmdprd  20011  dprd2da  20019  dmdprdpr  20026  issubrg3  20577  ishil2  21699  obslbs  21710  iscld2  22993  isperf3  23118  cncnp2  23246  cnnei  23247  trfbas2  23808  flimrest  23948  flfnei  23956  fclsrest  23989  tsmssubm  24108  isnghm2  24689  isnghm3  24690  isnmhm2  24717  iscfil2  25233  caucfil  25250  ellimc2  25844  cnlimc  25855  lhop1  25981  dvfsumlem1  25993  fsumharmonic  26975  fsumvma  27176  fsumvma2  27177  vmasum  27179  chpchtsum  27182  chpub  27183  rpvmasum2  27475  dchrisum0lem1  27479  dirith  27492  uvtx2vtx1edg  29467  uvtx2vtx1edgb  29468  iscplgrnb  29485  frgr3v  30345  adjeu  31960  suppiniseg  32759  suppss3  32796  nndiffz1  32859  indpreima  32925  islinds5  33427  fsumcvg4  34094  qqhval2lem  34125  eulerpartlemf  34514  elorvc  34604  hashreprin  34764  neibastop3  36544  relowlpssretop  37680  sstotbnd2  38095  isbnd3b  38106  lshpkr  39563  isat2  39733  islln4  39953  islpln4  39977  islvol4  40020  islhp2  40443  pw2f1o2val2  43468  modelaxreplem3  45407  rfcnpre1  45450  rfcnpre2  45462  joindm3  49444  meetdm3  49446  catprsc  49488