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  8998  eluz  12749  elicc4  13316  s111  14522  limsupgle  15384  lo1resb  15471  o1resb  15473  isercolllem2  15573  divalgmodcl  16318  ismri2  17538  acsfiel2  17561  eqglact  19058  eqgid  19059  cntzel  19202  dprdsubg  19905  subgdmdprd  19915  dprd2da  19923  dmdprdpr  19930  issubrg3  20485  ishil2  21626  obslbs  21637  iscld2  22913  isperf3  23038  cncnp2  23166  cnnei  23167  trfbas2  23728  flimrest  23868  flfnei  23876  fclsrest  23909  tsmssubm  24028  isnghm2  24610  isnghm3  24611  isnmhm2  24638  iscfil2  25164  caucfil  25181  ellimc2  25776  cnlimc  25787  lhop1  25917  dvfsumlem1  25930  fsumharmonic  26920  fsumvma  27122  fsumvma2  27123  vmasum  27125  chpchtsum  27128  chpub  27129  rpvmasum2  27421  dchrisum0lem1  27425  dirith  27438  uvtx2vtx1edg  29343  uvtx2vtx1edgb  29344  iscplgrnb  29361  frgr3v  30219  adjeu  31833  suppiniseg  32628  suppss3  32667  nndiffz1  32729  indpreima  32808  islinds5  33304  fsumcvg4  33917  qqhval2lem  33948  eulerpartlemf  34338  elorvc  34428  hashreprin  34588  neibastop3  36336  relowlpssretop  37338  sstotbnd2  37754  isbnd3b  37765  lshpkr  39096  isat2  39266  islln4  39486  islpln4  39510  islvol4  39553  islhp2  39976  pw2f1o2val2  43013  modelaxreplem3  44954  rfcnpre1  44997  rfcnpre2  45009  joindm3  48953  meetdm3  48955  catprsc  48998