|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > syl21anbrc | Structured version Visualization version GIF version | ||
| Description: Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.) | 
| Ref | Expression | 
|---|---|
| syl21anbrc.1 | ⊢ (𝜑 → 𝜓) | 
| syl21anbrc.2 | ⊢ (𝜑 → 𝜒) | 
| syl21anbrc.3 | ⊢ (𝜑 → 𝜃) | 
| syl21anbrc.4 | ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | 
| Ref | Expression | 
|---|---|
| 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 ⊢ (𝜑 → 𝜏) | 
| Colors of variables: wff setvar class | 
| 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 8325 erinxp 8831 frrlem15 9797 fpwwe2lem11 10681 nqerf 10970 nqerid 10973 genpcl 11048 nqpr 11054 ltexprlem5 11080 psss 18625 psssdm2 18626 ismhmd 18799 idmhm 18808 resmhm2b 18835 prdspjmhm 18842 pwsdiagmhm 18844 pwsco1mhm 18845 pwsco2mhm 18846 frmdup1 18877 mhmfmhm 19083 isghmd 19243 ghmmhm 19244 idghm 19249 symgsubmefmndALT 19421 lactghmga 19423 frgpmhm 19783 frgpuplem 19790 mulgmhm 19845 isrhm2d 20487 idrhm 20490 pwsco1rhm 20502 pwsco2rhm 20503 subrgid 20573 issubrg2 20592 subsubrg 20598 pwsdiagrhm 20607 islmhmd 21038 reslmhm 21051 rngqiprngho 21313 issubassa 21887 subrgpsr 21998 mat1mhm 22490 mat1rhm 22491 scmatmhm 22540 scmatrhm 22541 mat2pmatmhm 22739 mat2pmatrhm 22740 m2cpmrhm 22752 pm2mpmhm 22826 pm2mprhm 22827 ptpjcn 23619 idnmhm 24775 pi1cpbl 25077 pi1grplem 25082 pi1xfr 25088 pi1coghm 25094 vitalilem1 25643 vitalilem3 25645 ssltd 27836 sssslt1 27840 sssslt2 27841 syl22anbrc 32474 fldgenfldext 33718 weiunso 36467 prjspertr 42615 prjspvs 42620 0prjspnrel 42637 nla0002 43437 nla0003 43438 clnbgrvtxel 47816 clnbgredg 47826 | 
| Copyright terms: Public domain | W3C validator |