Theorem baibd 537

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  pw2f1olem  8333  eluz  11982  elicc4  12528  s111  13675  limsupgle  14585  lo1resb  14672  o1resb  14674  isercolllem2  14773  divalgmodcl  15504  ismri2  16645  acsfiel2  16668  issect2  16766  eqglact  17996  eqgid  17997  cntzel  18106  dprdsubg  18777  subgdmdprd  18787  dprd2da  18795  dmdprdpr  18802  issubrg3  19164  ishil2  20426  obslbs  20437  iscld2  21203  isperf3  21328  cncnp2  21456  cnnei  21457  trfbas2  22017  flimrest  22157  flfnei  22165  fclsrest  22198  tsmssubm  22316  isnghm2  22898  isnghm3  22899  isnmhm2  22926  iscfil2  23434  caucfil  23451  ellimc2  24040  cnlimc  24051  lhop1  24176  dvfsumlem1  24188  fsumharmonic  25151  fsumvma  25351  fsumvma2  25352  vmasum  25354  chpchtsum  25357  chpub  25358  rpvmasum2  25614  dchrisum0lem1  25618  dirith  25631  uvtx2vtx1edg  26696  uvtx2vtx1edgb  26697  iscplgrnb  26714  frgr3v  27656  adjeu  29303  suppss3  30050  nndiffz1  30095  fsumcvg4  30541  qqhval2lem  30570  indpreima  30632  eulerpartlemf  30977  elorvc  31067  hashreprin  31247  neibastop3  32895  relowlpssretop  33757  sstotbnd2  34115  isbnd3b  34126  lshpkr  35192  isat2  35362  islln4  35582  islpln4  35606  islvol4  35649  islhp2  36072  pw2f1o2val2  38450  rfcnpre1  39996  rfcnpre2  40008