![]() |
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 515 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
5 | syl21anbrc.4 | . 2 ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
6 | 4, 5 | sylibr 233 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: fprlem1 8223 erinxp 8688 frrlem15 9651 fpwwe2lem11 10535 nqerf 10824 nqerid 10827 genpcl 10902 nqpr 10908 ltexprlem5 10934 psss 18429 psssdm2 18430 ismhmd 18564 idmhm 18571 resmhm2b 18593 prdspjmhm 18599 pwsdiagmhm 18601 pwsco1mhm 18602 pwsco2mhm 18603 frmdup1 18634 mhmfmhm 18829 isghmd 18976 ghmmhm 18977 idghm 18982 symgsubmefmndALT 19144 lactghmga 19146 frgpmhm 19506 frgpuplem 19513 mulgmhm 19565 isrhm2d 20113 idrhm 20116 pwsco1rhm 20125 pwsco2rhm 20126 subrgid 20177 issubrg2 20195 subsubrg 20201 pwsdiagrhm 20209 islmhmd 20453 reslmhm 20466 issubassa 21225 subrgpsr 21340 mat1mhm 21785 mat1rhm 21786 scmatmhm 21835 scmatrhm 21836 mat2pmatmhm 22034 mat2pmatrhm 22035 m2cpmrhm 22047 pm2mpmhm 22121 pm2mprhm 22122 ptpjcn 22914 idnmhm 24070 pi1cpbl 24359 pi1grplem 24364 pi1xfr 24370 pi1coghm 24376 vitalilem1 24924 vitalilem3 24926 ssltd 27083 sssslt1 27086 sssslt2 27087 prjspertr 40852 prjspvs 40857 0prjspnrel 40874 nla0002 41607 nla0003 41608 |
Copyright terms: Public domain | W3C validator |