Theorem syl21anbrc 1345

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 514	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		syl21anbrc.4	. 2 ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
6	4, 5	sylibr 234	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:  fprlem1  8238  erinxp  8723  frrlem15  9659  fpwwe2lem11  10541  nqerf  10830  nqerid  10833  genpcl  10908  nqpr  10914  ltexprlem5  10940  psss  18490  psssdm2  18491  ismhmd  18698  idmhm  18707  resmhm2b  18734  prdspjmhm  18741  pwsdiagmhm  18743  pwsco1mhm  18744  pwsco2mhm  18745  frmdup1  18776  mhmfmhm  18982  isghmd  19141  ghmmhm  19142  idghm  19147  symgsubmefmndALT  19319  lactghmga  19321  frgpmhm  19681  frgpuplem  19688  mulgmhm  19743  isrhm2d  20408  idrhm  20411  pwsco1rhm  20421  pwsco2rhm  20422  subrgid  20492  issubrg2  20511  subsubrg  20517  pwsdiagrhm  20526  islmhmd  20977  reslmhm  20990  rngqiprngho  21244  issubassa  21808  subrgpsr  21918  mat1mhm  22402  mat1rhm  22403  scmatmhm  22452  scmatrhm  22453  mat2pmatmhm  22651  mat2pmatrhm  22652  m2cpmrhm  22664  pm2mpmhm  22738  pm2mprhm  22739  ptpjcn  23529  idnmhm  24672  pi1cpbl  24974  pi1grplem  24979  pi1xfr  24985  pi1coghm  24991  vitalilem1  25539  vitalilem3  25541  ssltd  27734  sssslt1  27739  sssslt2  27740  syl22anbrc  32438  fldgenfldext  33704  weiunso  36533  prjspertr  42726  prjspvs  42731  0prjspnrel  42748  nla0002  43544  nla0003  43545  clnbgrvtxel  47956  clnbgredg  47967