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  9142  eluz  12917  elicc4  13474  s111  14663  limsupgle  15523  lo1resb  15610  o1resb  15612  isercolllem2  15714  divalgmodcl  16455  ismri2  17690  acsfiel2  17713  eqglact  19219  eqgid  19220  cntzel  19363  dprdsubg  20068  subgdmdprd  20078  dprd2da  20086  dmdprdpr  20093  issubrg3  20628  ishil2  21762  obslbs  21773  iscld2  23057  isperf3  23182  cncnp2  23310  cnnei  23311  trfbas2  23872  flimrest  24012  flfnei  24020  fclsrest  24053  tsmssubm  24172  isnghm2  24766  isnghm3  24767  isnmhm2  24794  iscfil2  25319  caucfil  25336  ellimc2  25932  cnlimc  25943  lhop1  26073  dvfsumlem1  26086  fsumharmonic  27073  fsumvma  27275  fsumvma2  27276  vmasum  27278  chpchtsum  27281  chpub  27282  rpvmasum2  27574  dchrisum0lem1  27578  dirith  27591  uvtx2vtx1edg  29433  uvtx2vtx1edgb  29434  iscplgrnb  29451  frgr3v  30307  adjeu  31921  suppiniseg  32698  suppss3  32738  nndiffz1  32791  islinds5  33360  fsumcvg4  33896  qqhval2lem  33927  indpreima  33989  eulerpartlemf  34335  elorvc  34424  hashreprin  34597  neibastop3  36328  relowlpssretop  37330  sstotbnd2  37734  isbnd3b  37745  lshpkr  39073  isat2  39243  islln4  39464  islpln4  39488  islvol4  39531  islhp2  39954  pw2f1o2val2  42997  rfcnpre1  44919  rfcnpre2  44931  joindm3  48649  meetdm3  48651  catprsc  48680