Theorem sylanblrc 581

Description: Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.)

Hypotheses

Ref	Expression
sylanblrc.1	⊢ (𝜑 → 𝜓)
sylanblrc.2	⊢ 𝜒
sylanblrc.3	⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
sylanblrc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylanblrc

Step	Hyp	Ref	Expression
1		sylanblrc.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylanblrc.2	. 2 ⊢ 𝜒
3		sylanblrc.3	. . 3 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
4	3	biimpri 220	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 2, 4	sylancl 577	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  fntp  6242  foimacnv  6455  respreima  6655  fpr  6733  fnprb  6791  curry1  7601  fnwelem  7624  wfrlem13  7765  tfrlem10  7821  oawordeulem  7975  oelim2  8016  oaabs2  8066  omabs  8068  ssdomg  8346  limenpsi  8482  dffi2  8676  gruina  10032  recmulnq  10178  reclem2pr  10262  climeu  14767  cosmul  15380  2ebits  15650  algcvgblem  15771  ismgmid  17726  mndideu  17766  ga0  18193  efgs1  18613  distopon  21303  dfac14  21924  ptcmplem5  22362  sszcld  23122  itg11  23989  axlowdimlem13  26437  nbusgredgeu  26845  1trld  27665  1stmbfm  31163  2ndmbfm  31164  bnj150  31795  satf0n0  32188  frrlem12  32655  bj-projval  33826  exidu1  34576  rngoideu  34623  rfcnpre1  40695  funressnvmoOLD  42686