Theorem baibd 946

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ 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 196  df-an 385

This theorem is referenced by:  pw2f1olem  7949  eluz  11577  elicc4  12111  s111  13248  limsupgle  14056  lo1resb  14143  o1resb  14145  isercolllem2  14244  divalgmodcl  14969  ismri2  16115  acsfiel2  16139  issect2  16237  eqglact  17468  eqgid  17469  cntzel  17579  dprdsubg  18246  subgdmdprd  18256  dprd2da  18264  dmdprdpr  18271  issubrg3  18631  ishil2  19882  obslbs  19893  iscld2  20642  isperf3  20767  cncnp2  20895  cnnei  20896  trfbas2  21457  flimrest  21597  flfnei  21605  fclsrest  21638  tsmssubm  21756  isnghm2  22338  isnghm3  22339  isnmhm2  22366  iscfil2  22872  caucfil  22889  ellimc2  23447  cnlimc  23458  lhop1  23581  dvfsumlem1  23593  fsumharmonic  24538  fsumvma  24738  fsumvma2  24739  vmasum  24741  chpchtsum  24744  chpub  24745  rpvmasum2  25001  dchrisum0lem1  25005  dirith  25018  cusgrauvtxb  26024  adjeu  28132  suppss3  28890  nndiffz1  28936  fsumcvg4  29324  qqhval2lem  29353  indpreima  29414  eulerpartlemf  29759  elorvc  29848  neibastop3  31527  relowlpssretop  32388  sstotbnd2  32743  isbnd3b  32754  lshpkr  33422  isat2  33592  islln4  33811  islpln4  33835  islvol4  33878  islhp2  34301  pw2f1o2val2  36625  rfcnpre1  38201  rfcnpre2  38213  uvtx2vtx1edg  40625  uvtx2vtx1edgb  40626  iscplgrnb  40638  frgr3v  41445