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  18505  psssdm2  18506  ismhmd  18679  idmhm  18688  resmhm2b  18715  prdspjmhm  18722  pwsdiagmhm  18724  pwsco1mhm  18725  pwsco2mhm  18726  frmdup1  18757  mhmfmhm  18963  isghmd  19123  ghmmhm  19124  idghm  19129  symgsubmefmndALT  19301  lactghmga  19303  frgpmhm  19663  frgpuplem  19670  mulgmhm  19725  isrhm2d  20391  idrhm  20394  pwsco1rhm  20406  pwsco2rhm  20407  subrgid  20477  issubrg2  20496  subsubrg  20502  pwsdiagrhm  20511  islmhmd  20962  reslmhm  20975  rngqiprngho  21229  issubassa  21793  subrgpsr  21904  mat1mhm  22388  mat1rhm  22389  scmatmhm  22438  scmatrhm  22439  mat2pmatmhm  22637  mat2pmatrhm  22638  m2cpmrhm  22650  pm2mpmhm  22724  pm2mprhm  22725  ptpjcn  23515  idnmhm  24659  pi1cpbl  24961  pi1grplem  24966  pi1xfr  24972  pi1coghm  24978  vitalilem1  25526  vitalilem3  25528  ssltd  27721  sssslt1  27725  sssslt2  27726  syl22anbrc  32418  fldgenfldext  33654  weiunso  36459  prjspertr  42598  prjspvs  42603  0prjspnrel  42620  nla0002  43417  nla0003  43418  clnbgrvtxel  47833  clnbgredg  47844