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  8240  erinxp  8725  frrlem15  9672  fpwwe2lem11  10554  nqerf  10843  nqerid  10846  genpcl  10921  nqpr  10927  ltexprlem5  10953  psss  18504  psssdm2  18505  ismhmd  18678  idmhm  18687  resmhm2b  18714  prdspjmhm  18721  pwsdiagmhm  18723  pwsco1mhm  18724  pwsco2mhm  18725  frmdup1  18756  mhmfmhm  18962  isghmd  19122  ghmmhm  19123  idghm  19128  symgsubmefmndALT  19300  lactghmga  19302  frgpmhm  19662  frgpuplem  19669  mulgmhm  19724  isrhm2d  20390  idrhm  20393  pwsco1rhm  20405  pwsco2rhm  20406  subrgid  20476  issubrg2  20495  subsubrg  20501  pwsdiagrhm  20510  islmhmd  20961  reslmhm  20974  rngqiprngho  21228  issubassa  21792  subrgpsr  21903  mat1mhm  22387  mat1rhm  22388  scmatmhm  22437  scmatrhm  22438  mat2pmatmhm  22636  mat2pmatrhm  22637  m2cpmrhm  22649  pm2mpmhm  22723  pm2mprhm  22724  ptpjcn  23514  idnmhm  24658  pi1cpbl  24960  pi1grplem  24965  pi1xfr  24971  pi1coghm  24977  vitalilem1  25525  vitalilem3  25527  ssltd  27720  sssslt1  27724  sssslt2  27725  syl22anbrc  32417  fldgenfldext  33642  weiunso  36442  prjspertr  42581  prjspvs  42586  0prjspnrel  42603  nla0002  43400  nla0003  43401  clnbgrvtxel  47817  clnbgredg  47828