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  9090  eluz  12866  elicc4  13430  s111  14633  limsupgle  15493  lo1resb  15580  o1resb  15582  isercolllem2  15682  divalgmodcl  16426  ismri2  17644  acsfiel2  17667  eqglact  19162  eqgid  19163  cntzel  19306  dprdsubg  20007  subgdmdprd  20017  dprd2da  20025  dmdprdpr  20032  issubrg3  20560  ishil2  21679  obslbs  21690  iscld2  22966  isperf3  23091  cncnp2  23219  cnnei  23220  trfbas2  23781  flimrest  23921  flfnei  23929  fclsrest  23962  tsmssubm  24081  isnghm2  24663  isnghm3  24664  isnmhm2  24691  iscfil2  25218  caucfil  25235  ellimc2  25830  cnlimc  25841  lhop1  25971  dvfsumlem1  25984  fsumharmonic  26974  fsumvma  27176  fsumvma2  27177  vmasum  27179  chpchtsum  27182  chpub  27183  rpvmasum2  27475  dchrisum0lem1  27479  dirith  27492  uvtx2vtx1edg  29377  uvtx2vtx1edgb  29378  iscplgrnb  29395  frgr3v  30256  adjeu  31870  suppiniseg  32663  suppss3  32701  nndiffz1  32763  indpreima  32842  islinds5  33382  fsumcvg4  33981  qqhval2lem  34012  eulerpartlemf  34402  elorvc  34492  hashreprin  34652  neibastop3  36380  relowlpssretop  37382  sstotbnd2  37798  isbnd3b  37809  lshpkr  39135  isat2  39305  islln4  39526  islpln4  39550  islvol4  39593  islhp2  40016  pw2f1o2val2  43064  modelaxreplem3  45005  rfcnpre1  45043  rfcnpre2  45055  joindm3  48943  meetdm3  48945  catprsc  48988