Theorem baibd 547

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  rbaibd  548  bian1d  588  pw2f1olem  9053  eluz  12853  elicc4  13417  s111  14629  limsupgle  15504  lo1resb  15591  o1resb  15593  isercolllem2  15693  divalgmodcl  16441  ismri2  17664  acsfiel2  17687  eqglact  19220  eqgid  19221  cntzel  19363  dprdsubg  20066  subgdmdprd  20076  dprd2da  20084  dmdprdpr  20091  issubrg3  20646  ishil2  21768  obslbs  21779  iscld2  23085  isperf3  23210  cncnp2  23338  cnnei  23339  trfbas2  23900  flimrest  24040  flfnei  24048  fclsrest  24081  tsmssubm  24200  isnghm2  24781  isnghm3  24782  isnmhm2  24809  iscfil2  25325  caucfil  25342  ellimc2  25936  cnlimc  25947  lhop1  26073  dvfsumlem1  26085  fsumharmonic  27073  fsumvma  27274  fsumvma2  27275  vmasum  27277  chpchtsum  27280  chpub  27281  rpvmasum2  27573  dchrisum0lem1  27577  dirith  27590  uvtx2vtx1edg  29596  uvtx2vtx1edgb  29597  iscplgrnb  29614  frgr3v  30474  adjeu  32089  suppiniseg  32885  suppss3  32922  nndiffz1  32985  indpreima  33040  islinds5  33550  fsumcvg4  34244  qqhval2lem  34275  eulerpartlemf  34664  elorvc  34754  hashreprin  34911  neibastop3  36719  relowlpssretop  37855  sstotbnd2  38270  isbnd3b  38281  lshpkr  39738  isat2  39908  islln4  40128  islpln4  40152  islvol4  40195  islhp2  40618  pw2f1o2val2  43614  modelaxreplem3  45553  rfcnpre1  45596  rfcnpre2  45608  joindm3  49587  meetdm3  49589  catprsc  49631