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 517 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
5 | syl21anbrc.4 | . 2 ⊢ (𝜏 ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃)) | |
6 | 4, 5 | sylibr 236 | 1 ⊢ (𝜑 → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: erinxp 8371 fpwwe2lem12 10063 nqerf 10352 nqerid 10355 genpcl 10430 nqpr 10436 ltexprlem5 10462 psss 17824 psssdm2 17825 idmhm 17965 resmhm2b 17987 prdspjmhm 17993 pwsdiagmhm 17995 pwsco1mhm 17996 pwsco2mhm 17997 frmdup1 18029 mhmfmhm 18222 isghmd 18367 ghmmhm 18368 idghm 18373 symgsubmefmndALT 18531 lactghmga 18533 frgpmhm 18891 frgpuplem 18898 mulgmhm 18948 isrhm2d 19480 idrhm 19483 pwsco1rhm 19490 pwsco2rhm 19491 subrgid 19537 issubrg2 19555 subsubrg 19561 pwsdiagrhm 19569 islmhmd 19811 reslmhm 19824 issubassa 20098 subrgpsr 20199 mat1mhm 21093 mat1rhm 21094 scmatmhm 21143 scmatrhm 21144 mat2pmatmhm 21341 mat2pmatrhm 21342 m2cpmrhm 21354 pm2mpmhm 21428 pm2mprhm 21429 ptpjcn 22219 idnmhm 23363 pi1cpbl 23648 pi1grplem 23653 pi1xfr 23659 pi1coghm 23665 vitalilem1 24209 vitalilem3 24211 fprlem1 33137 frrlem15 33142 sssslt1 33260 sssslt2 33261 prjspertr 39275 prjspvs 39280 0prjspnrel 39289 |
Copyright terms: Public domain | W3C validator |