Theorem syl21anbrc 1346

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  8252  erinxp  8740  frrlem15  9681  fpwwe2lem11  10564  nqerf  10853  nqerid  10856  genpcl  10931  nqpr  10937  ltexprlem5  10963  psss  18515  psssdm2  18516  ismhmd  18723  idmhm  18732  resmhm2b  18759  prdspjmhm  18766  pwsdiagmhm  18768  pwsco1mhm  18769  pwsco2mhm  18770  frmdup1  18801  mhmfmhm  19007  isghmd  19166  ghmmhm  19167  idghm  19172  symgsubmefmndALT  19344  lactghmga  19346  frgpmhm  19706  frgpuplem  19713  mulgmhm  19768  isrhm2d  20434  idrhm  20437  pwsco1rhm  20447  pwsco2rhm  20448  subrgid  20518  issubrg2  20537  subsubrg  20543  pwsdiagrhm  20552  islmhmd  21003  reslmhm  21016  rngqiprngho  21270  issubassa  21834  subrgpsr  21945  mat1mhm  22440  mat1rhm  22441  scmatmhm  22490  scmatrhm  22491  mat2pmatmhm  22689  mat2pmatrhm  22690  m2cpmrhm  22702  pm2mpmhm  22776  pm2mprhm  22777  ptpjcn  23567  idnmhm  24710  pi1cpbl  25012  pi1grplem  25017  pi1xfr  25023  pi1coghm  25029  vitalilem1  25577  vitalilem3  25579  sltsd  27776  ssslts1  27781  ssslts2  27782  syl22anbrc  32541  fldgenfldext  33845  weiunso  36679  prjspertr  42960  prjspvs  42965  0prjspnrel  42982  nla0002  43777  nla0003  43778  clnbgrvtxel  48186  clnbgredg  48197