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  9007  eluz  12763  elicc4  13327  s111  14537  limsupgle  15398  lo1resb  15485  o1resb  15487  isercolllem2  15587  divalgmodcl  16332  ismri2  17553  acsfiel2  17576  eqglact  19106  eqgid  19107  cntzel  19250  dprdsubg  19953  subgdmdprd  19963  dprd2da  19971  dmdprdpr  19978  issubrg3  20531  ishil2  21672  obslbs  21683  iscld2  22970  isperf3  23095  cncnp2  23223  cnnei  23224  trfbas2  23785  flimrest  23925  flfnei  23933  fclsrest  23966  tsmssubm  24085  isnghm2  24666  isnghm3  24667  isnmhm2  24694  iscfil2  25220  caucfil  25237  ellimc2  25832  cnlimc  25843  lhop1  25973  dvfsumlem1  25986  fsumharmonic  26976  fsumvma  27178  fsumvma2  27179  vmasum  27181  chpchtsum  27184  chpub  27185  rpvmasum2  27477  dchrisum0lem1  27481  dirith  27494  uvtx2vtx1edg  29420  uvtx2vtx1edgb  29421  iscplgrnb  29438  frgr3v  30299  adjeu  31913  suppiniseg  32714  suppss3  32751  nndiffz1  32815  indpreima  32896  islinds5  33397  fsumcvg4  34056  qqhval2lem  34087  eulerpartlemf  34476  elorvc  34566  hashreprin  34726  neibastop3  36505  relowlpssretop  37508  sstotbnd2  37914  isbnd3b  37925  lshpkr  39316  isat2  39486  islln4  39706  islpln4  39730  islvol4  39773  islhp2  40196  pw2f1o2val2  43224  modelaxreplem3  45163  rfcnpre1  45206  rfcnpre2  45218  joindm3  49156  meetdm3  49158  catprsc  49200