Theorem baibd 968

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 524	. . 3 ⊢ (𝜒 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
3	2	bicomd 213	. 2 ⊢ (𝜒 → ((𝜒 ∧ 𝜃) ↔ 𝜃))
4	1, 3	sylan9bb 736	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  pw2f1olem  8105  eluz  11739  elicc4  12278  s111  13432  limsupgle  14252  lo1resb  14339  o1resb  14341  isercolllem2  14440  divalgmodcl  15178  ismri2  16339  acsfiel2  16363  issect2  16461  eqglact  17692  eqgid  17693  cntzel  17802  dprdsubg  18469  subgdmdprd  18479  dprd2da  18487  dmdprdpr  18494  issubrg3  18856  ishil2  20111  obslbs  20122  iscld2  20880  isperf3  21005  cncnp2  21133  cnnei  21134  trfbas2  21694  flimrest  21834  flfnei  21842  fclsrest  21875  tsmssubm  21993  isnghm2  22575  isnghm3  22576  isnmhm2  22603  iscfil2  23110  caucfil  23127  ellimc2  23686  cnlimc  23697  lhop1  23822  dvfsumlem1  23834  fsumharmonic  24783  fsumvma  24983  fsumvma2  24984  vmasum  24986  chpchtsum  24989  chpub  24990  rpvmasum2  25246  dchrisum0lem1  25250  dirith  25263  uvtx2vtx1edg  26349  uvtx2vtx1edgb  26350  iscplgrnb  26368  frgr3v  27255  adjeu  28876  suppss3  29630  nndiffz1  29676  fsumcvg4  30124  qqhval2lem  30153  indpreima  30215  eulerpartlemf  30560  elorvc  30649  hashreprin  30826  neibastop3  32482  relowlpssretop  33342  sstotbnd2  33703  isbnd3b  33714  lshpkr  34722  isat2  34892  islln4  35111  islpln4  35135  islvol4  35178  islhp2  35601  pw2f1o2val2  37924  rfcnpre1  39492  rfcnpre2  39504