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  9045  eluz  12807  elicc4  13374  s111  14580  limsupgle  15443  lo1resb  15530  o1resb  15532  isercolllem2  15632  divalgmodcl  16377  ismri2  17593  acsfiel2  17616  eqglact  19111  eqgid  19112  cntzel  19255  dprdsubg  19956  subgdmdprd  19966  dprd2da  19974  dmdprdpr  19981  issubrg3  20509  ishil2  21628  obslbs  21639  iscld2  22915  isperf3  23040  cncnp2  23168  cnnei  23169  trfbas2  23730  flimrest  23870  flfnei  23878  fclsrest  23911  tsmssubm  24030  isnghm2  24612  isnghm3  24613  isnmhm2  24640  iscfil2  25166  caucfil  25183  ellimc2  25778  cnlimc  25789  lhop1  25919  dvfsumlem1  25932  fsumharmonic  26922  fsumvma  27124  fsumvma2  27125  vmasum  27127  chpchtsum  27130  chpub  27131  rpvmasum2  27423  dchrisum0lem1  27427  dirith  27440  uvtx2vtx1edg  29325  uvtx2vtx1edgb  29326  iscplgrnb  29343  frgr3v  30204  adjeu  31818  suppiniseg  32609  suppss3  32647  nndiffz1  32709  indpreima  32788  islinds5  33338  fsumcvg4  33940  qqhval2lem  33971  eulerpartlemf  34361  elorvc  34451  hashreprin  34611  neibastop3  36350  relowlpssretop  37352  sstotbnd2  37768  isbnd3b  37779  lshpkr  39110  isat2  39280  islln4  39501  islpln4  39525  islvol4  39568  islhp2  39991  pw2f1o2val2  43029  modelaxreplem3  44970  rfcnpre1  45013  rfcnpre2  45025  joindm3  48957  meetdm3  48959  catprsc  49002