Theorem baibd 544

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  rbaibd  545  bian1d  585  pw2f1olem  9009  eluz  12793  elicc4  13357  s111  14569  limsupgle  15430  lo1resb  15517  o1resb  15519  isercolllem2  15619  divalgmodcl  16367  ismri2  17589  acsfiel2  17612  eqglact  19145  eqgid  19146  cntzel  19289  dprdsubg  19992  subgdmdprd  20002  dprd2da  20010  dmdprdpr  20017  issubrg3  20572  ishil2  21694  obslbs  21705  iscld2  23011  isperf3  23136  cncnp2  23264  cnnei  23265  trfbas2  23826  flimrest  23966  flfnei  23974  fclsrest  24007  tsmssubm  24126  isnghm2  24707  isnghm3  24708  isnmhm2  24735  iscfil2  25251  caucfil  25268  ellimc2  25862  cnlimc  25873  lhop1  25999  dvfsumlem1  26011  fsumharmonic  26993  fsumvma  27194  fsumvma2  27195  vmasum  27197  chpchtsum  27200  chpub  27201  rpvmasum2  27493  dchrisum0lem1  27497  dirith  27510  uvtx2vtx1edg  29485  uvtx2vtx1edgb  29486  iscplgrnb  29503  frgr3v  30363  adjeu  31978  suppiniseg  32778  suppss3  32815  nndiffz1  32878  indpreima  32944  islinds5  33450  fsumcvg4  34134  qqhval2lem  34165  eulerpartlemf  34554  elorvc  34644  hashreprin  34804  neibastop3  36590  relowlpssretop  37726  sstotbnd2  38141  isbnd3b  38152  lshpkr  39609  isat2  39779  islln4  39999  islpln4  40023  islvol4  40066  islhp2  40489  pw2f1o2val2  43485  modelaxreplem3  45424  rfcnpre1  45467  rfcnpre2  45479  joindm3  49459  meetdm3  49461  catprsc  49503