Theorem syl21anbrc 1343

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  8324  erinxp  8830  frrlem15  9795  fpwwe2lem11  10679  nqerf  10968  nqerid  10971  genpcl  11046  nqpr  11052  ltexprlem5  11078  psss  18638  psssdm2  18639  ismhmd  18812  idmhm  18821  resmhm2b  18848  prdspjmhm  18855  pwsdiagmhm  18857  pwsco1mhm  18858  pwsco2mhm  18859  frmdup1  18890  mhmfmhm  19096  isghmd  19256  ghmmhm  19257  idghm  19262  symgsubmefmndALT  19436  lactghmga  19438  frgpmhm  19798  frgpuplem  19805  mulgmhm  19860  isrhm2d  20504  idrhm  20507  pwsco1rhm  20519  pwsco2rhm  20520  subrgid  20590  issubrg2  20609  subsubrg  20615  pwsdiagrhm  20624  islmhmd  21056  reslmhm  21069  rngqiprngho  21331  issubassa  21905  subrgpsr  22016  mat1mhm  22506  mat1rhm  22507  scmatmhm  22556  scmatrhm  22557  mat2pmatmhm  22755  mat2pmatrhm  22756  m2cpmrhm  22768  pm2mpmhm  22842  pm2mprhm  22843  ptpjcn  23635  idnmhm  24791  pi1cpbl  25091  pi1grplem  25096  pi1xfr  25102  pi1coghm  25108  vitalilem1  25657  vitalilem3  25659  ssltd  27851  sssslt1  27855  sssslt2  27856  fldgenfldext  33693  weiunso  36449  prjspertr  42592  prjspvs  42597  0prjspnrel  42614  nla0002  43414  nla0003  43415  clnbgrvtxel  47754  clnbgredg  47764