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  9009  eluz  12765  elicc4  13329  s111  14539  limsupgle  15400  lo1resb  15487  o1resb  15489  isercolllem2  15589  divalgmodcl  16334  ismri2  17555  acsfiel2  17578  eqglact  19108  eqgid  19109  cntzel  19252  dprdsubg  19955  subgdmdprd  19965  dprd2da  19973  dmdprdpr  19980  issubrg3  20533  ishil2  21674  obslbs  21685  iscld2  22972  isperf3  23097  cncnp2  23225  cnnei  23226  trfbas2  23787  flimrest  23927  flfnei  23935  fclsrest  23968  tsmssubm  24087  isnghm2  24668  isnghm3  24669  isnmhm2  24696  iscfil2  25222  caucfil  25239  ellimc2  25834  cnlimc  25845  lhop1  25975  dvfsumlem1  25988  fsumharmonic  26978  fsumvma  27180  fsumvma2  27181  vmasum  27183  chpchtsum  27186  chpub  27187  rpvmasum2  27479  dchrisum0lem1  27483  dirith  27496  uvtx2vtx1edg  29471  uvtx2vtx1edgb  29472  iscplgrnb  29489  frgr3v  30350  adjeu  31964  suppiniseg  32765  suppss3  32802  nndiffz1  32866  indpreima  32947  islinds5  33448  fsumcvg4  34107  qqhval2lem  34138  eulerpartlemf  34527  elorvc  34617  hashreprin  34777  neibastop3  36556  relowlpssretop  37569  sstotbnd2  37975  isbnd3b  37986  lshpkr  39377  isat2  39547  islln4  39767  islpln4  39791  islvol4  39834  islhp2  40257  pw2f1o2val2  43282  modelaxreplem3  45221  rfcnpre1  45264  rfcnpre2  45276  joindm3  49214  meetdm3  49216  catprsc  49258