Theorem syl21anbrc 1340

Description: Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.)

Hypotheses

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

Assertion

Ref	Expression
syl21anbrc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl21anbrc

Step	Hyp	Ref	Expression
1		syl21anbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl21anbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl21anbrc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca31 517	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anbrc.4	. 2 ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
6	4, 5	sylibr 236	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  erinxp  8371  fpwwe2lem12  10063  nqerf  10352  nqerid  10355  genpcl  10430  nqpr  10436  ltexprlem5  10462  psss  17824  psssdm2  17825  idmhm  17965  resmhm2b  17987  prdspjmhm  17993  pwsdiagmhm  17995  pwsco1mhm  17996  pwsco2mhm  17997  frmdup1  18029  mhmfmhm  18222  isghmd  18367  ghmmhm  18368  idghm  18373  symgsubmefmndALT  18531  lactghmga  18533  frgpmhm  18891  frgpuplem  18898  mulgmhm  18948  isrhm2d  19480  idrhm  19483  pwsco1rhm  19490  pwsco2rhm  19491  subrgid  19537  issubrg2  19555  subsubrg  19561  pwsdiagrhm  19569  islmhmd  19811  reslmhm  19824  issubassa  20098  subrgpsr  20199  mat1mhm  21093  mat1rhm  21094  scmatmhm  21143  scmatrhm  21144  mat2pmatmhm  21341  mat2pmatrhm  21342  m2cpmrhm  21354  pm2mpmhm  21428  pm2mprhm  21429  ptpjcn  22219  idnmhm  23363  pi1cpbl  23648  pi1grplem  23653  pi1xfr  23659  pi1coghm  23665  vitalilem1  24209  vitalilem3  24211  fprlem1  33137  frrlem15  33142  sssslt1  33260  sssslt2  33261  prjspertr  39304  prjspvs  39309  0prjspnrel  39318