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 518 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
5 | syl21anbrc.4 | . 2 ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
6 | 4, 5 | sylibr 237 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: fprlem1 8030 erinxp 8462 fpwwe2lem11 10238 nqerf 10527 nqerid 10530 genpcl 10605 nqpr 10611 ltexprlem5 10637 psss 18058 psssdm2 18059 idmhm 18199 resmhm2b 18221 prdspjmhm 18227 pwsdiagmhm 18229 pwsco1mhm 18230 pwsco2mhm 18231 frmdup1 18263 mhmfmhm 18458 isghmd 18603 ghmmhm 18604 idghm 18609 symgsubmefmndALT 18767 lactghmga 18769 frgpmhm 19127 frgpuplem 19134 mulgmhm 19185 isrhm2d 19720 idrhm 19723 pwsco1rhm 19730 pwsco2rhm 19731 subrgid 19774 issubrg2 19792 subsubrg 19798 pwsdiagrhm 19806 islmhmd 20048 reslmhm 20061 issubassa 20800 subrgpsr 20916 mat1mhm 21353 mat1rhm 21354 scmatmhm 21403 scmatrhm 21404 mat2pmatmhm 21602 mat2pmatrhm 21603 m2cpmrhm 21615 pm2mpmhm 21689 pm2mprhm 21690 ptpjcn 22480 idnmhm 23624 pi1cpbl 23913 pi1grplem 23918 pi1xfr 23924 pi1coghm 23930 vitalilem1 24477 vitalilem3 24479 frrlem15 33513 ssltd 33680 sssslt1 33683 sssslt2 33684 ismhmd 39903 prjspertr 40104 prjspvs 40109 0prjspnrel 40124 |
Copyright terms: Public domain | W3C validator |