Theorem baibd 541

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  rbaibd  542  pw2f1olem  8901  eluz  12642  elicc4  13192  s111  14365  limsupgle  15231  lo1resb  15318  o1resb  15320  isercolllem2  15422  divalgmodcl  16161  ismri2  17386  acsfiel2  17409  eqglact  18852  eqgid  18853  cntzel  18974  dprdsubg  19672  subgdmdprd  19682  dprd2da  19690  dmdprdpr  19697  issubrg3  20097  ishil2  20971  obslbs  20982  iscld2  22224  isperf3  22349  cncnp2  22477  cnnei  22478  trfbas2  23039  flimrest  23179  flfnei  23187  fclsrest  23220  tsmssubm  23339  isnghm2  23933  isnghm3  23934  isnmhm2  23961  iscfil2  24475  caucfil  24492  ellimc2  25086  cnlimc  25097  lhop1  25223  dvfsumlem1  25235  fsumharmonic  26206  fsumvma  26406  fsumvma2  26407  vmasum  26409  chpchtsum  26412  chpub  26413  rpvmasum2  26705  dchrisum0lem1  26709  dirith  26722  uvtx2vtx1edg  27810  uvtx2vtx1edgb  27811  iscplgrnb  27828  frgr3v  28684  adjeu  30296  suppiniseg  31065  suppss3  31104  nndiffz1  31152  islinds5  31608  fsumcvg4  31945  qqhval2lem  31976  indpreima  32038  eulerpartlemf  32382  elorvc  32471  hashreprin  32645  neibastop3  34596  relowlpssretop  35579  sstotbnd2  35976  isbnd3b  35987  lshpkr  37173  isat2  37343  islln4  37563  islpln4  37587  islvol4  37630  islhp2  38053  pw2f1o2val2  40900  rfcnpre1  42600  rfcnpre2  42612  joindm3  46321  meetdm3  46323  catprsc  46352