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  9116  eluz  12892  elicc4  13454  s111  14653  limsupgle  15513  lo1resb  15600  o1resb  15602  isercolllem2  15702  divalgmodcl  16444  ismri2  17675  acsfiel2  17698  eqglact  19197  eqgid  19198  cntzel  19341  dprdsubg  20044  subgdmdprd  20054  dprd2da  20062  dmdprdpr  20069  issubrg3  20600  ishil2  21739  obslbs  21750  iscld2  23036  isperf3  23161  cncnp2  23289  cnnei  23290  trfbas2  23851  flimrest  23991  flfnei  23999  fclsrest  24032  tsmssubm  24151  isnghm2  24745  isnghm3  24746  isnmhm2  24773  iscfil2  25300  caucfil  25317  ellimc2  25912  cnlimc  25923  lhop1  26053  dvfsumlem1  26066  fsumharmonic  27055  fsumvma  27257  fsumvma2  27258  vmasum  27260  chpchtsum  27263  chpub  27264  rpvmasum2  27556  dchrisum0lem1  27560  dirith  27573  uvtx2vtx1edg  29415  uvtx2vtx1edgb  29416  iscplgrnb  29433  frgr3v  30294  adjeu  31908  suppiniseg  32695  suppss3  32735  nndiffz1  32788  indpreima  32850  islinds5  33395  fsumcvg4  33949  qqhval2lem  33982  eulerpartlemf  34372  elorvc  34462  hashreprin  34635  neibastop3  36363  relowlpssretop  37365  sstotbnd2  37781  isbnd3b  37792  lshpkr  39118  isat2  39288  islln4  39509  islpln4  39533  islvol4  39576  islhp2  39999  pw2f1o2val2  43052  modelaxreplem3  44997  rfcnpre1  45024  rfcnpre2  45036  joindm3  48866  meetdm3  48868  catprsc  48902