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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  rbaibd  545  pw2f1olem  8642  eluz  12289  elicc4  12839  s111  14009  limsupgle  14875  lo1resb  14962  o1resb  14964  isercolllem2  15063  divalgmodcl  15801  ismri2  16954  acsfiel2  16977  eqglact  18391  eqgid  18392  cntzel  18513  dprdsubg  19207  subgdmdprd  19217  dprd2da  19225  dmdprdpr  19232  issubrg3  19624  ishil2  20477  obslbs  20488  iscld2  21721  isperf3  21846  cncnp2  21974  cnnei  21975  trfbas2  22536  flimrest  22676  flfnei  22684  fclsrest  22717  tsmssubm  22836  isnghm2  23419  isnghm3  23420  isnmhm2  23447  iscfil2  23959  caucfil  23976  ellimc2  24569  cnlimc  24580  lhop1  24706  dvfsumlem1  24718  fsumharmonic  25689  fsumvma  25889  fsumvma2  25890  vmasum  25892  chpchtsum  25895  chpub  25896  rpvmasum2  26188  dchrisum0lem1  26192  dirith  26205  uvtx2vtx1edg  27280  uvtx2vtx1edgb  27281  iscplgrnb  27298  frgr3v  28152  adjeu  29764  suppiniseg  30537  suppss3  30576  nndiffz1  30624  islinds5  31077  fsumcvg4  31414  qqhval2lem  31443  indpreima  31505  eulerpartlemf  31849  elorvc  31938  hashreprin  32112  neibastop3  34093  relowlpssretop  35054  sstotbnd2  35485  isbnd3b  35496  lshpkr  36686  isat2  36856  islln4  37076  islpln4  37100  islvol4  37143  islhp2  37566  pw2f1o2val2  40347  rfcnpre1  42014  rfcnpre2  42026