Theorem baibd 542

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  rbaibd  543  pw2f1olem  8615  eluz  12251  elicc4  12797  s111  13963  limsupgle  14828  lo1resb  14915  o1resb  14917  isercolllem2  15016  divalgmodcl  15752  ismri2  16897  acsfiel2  16920  eqglact  18325  eqgid  18326  cntzel  18447  dprdsubg  19140  subgdmdprd  19150  dprd2da  19158  dmdprdpr  19165  issubrg3  19557  ishil2  20857  obslbs  20868  iscld2  21630  isperf3  21755  cncnp2  21883  cnnei  21884  trfbas2  22445  flimrest  22585  flfnei  22593  fclsrest  22626  tsmssubm  22745  isnghm2  23327  isnghm3  23328  isnmhm2  23355  iscfil2  23863  caucfil  23880  ellimc2  24469  cnlimc  24480  lhop1  24605  dvfsumlem1  24617  fsumharmonic  25583  fsumvma  25783  fsumvma2  25784  vmasum  25786  chpchtsum  25789  chpub  25790  rpvmasum2  26082  dchrisum0lem1  26086  dirith  26099  uvtx2vtx1edg  27174  uvtx2vtx1edgb  27175  iscplgrnb  27192  frgr3v  28048  adjeu  29660  suppss3  30454  nndiffz1  30503  islinds5  30927  fsumcvg4  31188  qqhval2lem  31217  indpreima  31279  eulerpartlemf  31623  elorvc  31712  hashreprin  31886  neibastop3  33705  relowlpssretop  34639  sstotbnd2  35046  isbnd3b  35057  lshpkr  36247  isat2  36417  islln4  36637  islpln4  36661  islvol4  36704  islhp2  37127  pw2f1o2val2  39630  rfcnpre1  41269  rfcnpre2  41281