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  8994  eluz  12746  elicc4  13313  s111  14523  limsupgle  15384  lo1resb  15471  o1resb  15473  isercolllem2  15573  divalgmodcl  16318  ismri2  17538  acsfiel2  17561  eqglact  19091  eqgid  19092  cntzel  19235  dprdsubg  19938  subgdmdprd  19948  dprd2da  19956  dmdprdpr  19963  issubrg3  20515  ishil2  21656  obslbs  21667  iscld2  22943  isperf3  23068  cncnp2  23196  cnnei  23197  trfbas2  23758  flimrest  23898  flfnei  23906  fclsrest  23939  tsmssubm  24058  isnghm2  24639  isnghm3  24640  isnmhm2  24667  iscfil2  25193  caucfil  25210  ellimc2  25805  cnlimc  25816  lhop1  25946  dvfsumlem1  25959  fsumharmonic  26949  fsumvma  27151  fsumvma2  27152  vmasum  27154  chpchtsum  27157  chpub  27158  rpvmasum2  27450  dchrisum0lem1  27454  dirith  27467  uvtx2vtx1edg  29376  uvtx2vtx1edgb  29377  iscplgrnb  29394  frgr3v  30255  adjeu  31869  suppiniseg  32667  suppss3  32706  nndiffz1  32769  indpreima  32846  islinds5  33332  fsumcvg4  33963  qqhval2lem  33994  eulerpartlemf  34383  elorvc  34473  hashreprin  34633  neibastop3  36404  relowlpssretop  37406  sstotbnd2  37822  isbnd3b  37833  lshpkr  39164  isat2  39334  islln4  39554  islpln4  39578  islvol4  39621  islhp2  40044  pw2f1o2val2  43081  modelaxreplem3  45021  rfcnpre1  45064  rfcnpre2  45076  joindm3  49008  meetdm3  49010  catprsc  49053