Theorem baibd 549

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rbaibd  550  bian1d  591  pw2f1olem  9111  eluz  12989  elicc4  13554  s111  14774  limsupgle  15656  lo1resb  15743  o1resb  15745  isercolllem2  15845  divalgmodcl  16589  ismri2  17818  acsfiel2  17841  eqglact  19403  eqgid  19404  cntzel  19549  dprdsubg  20252  subgdmdprd  20262  dprd2da  20270  dmdprdpr  20277  issubrg3  20864  ishil2  22037  obslbs  22048  iscld2  23358  isperf3  23483  cncnp2  23611  cnnei  23612  trfbas2  24174  flimrest  24314  flfnei  24322  fclsrest  24355  tsmssubm  24474  isnghm2  25055  isnghm3  25056  isnmhm2  25083  iscfil2  25599  caucfil  25616  ellimc2  26209  cnlimc  26220  lhop1  26346  dvfsumlem1  26358  fsumharmonic  27351  fsumvma  27552  fsumvma2  27553  vmasum  27555  chpchtsum  27558  chpub  27559  rpvmasum2  27851  dchrisum0lem1  27855  dirith  27868  uvtx2vtx1edg  29991  uvtx2vtx1edgb  29992  iscplgrnb  30009  frgr3v  30888  adjeu  32503  suppiniseg  33333  suppss3  33368  nndiffz1  33431  indpreima  33485  islinds5  33976  fsumcvg4  34635  qqhval2lem  34666  eulerpartlemf  35055  elorvc  35145  hashreprin  35302  neibastop3  37277  relowlpssretop  38427  sstotbnd2  38848  isbnd3b  38859  lshpkr  40314  isat2  40484  islln4  40704  islpln4  40728  islvol4  40771  islhp2  41194  pw2f1o2val2  44187  modelaxreplem3  46109  rfcnpre1  46175  rfcnpre2  46187  joindm3  50222  meetdm3  50224  catprsc  50266