| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > syl2and | Structured version Visualization version GIF version | ||
| Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
| Ref | Expression |
|---|---|
| syl2and.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
| syl2and.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
| syl2and.3 | ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂)) |
| Ref | Expression |
|---|---|
| syl2and | ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | syl2and.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
| 2 | syl2and.2 | . . 3 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
| 3 | syl2and.3 | . . 3 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂)) | |
| 4 | 2, 3 | sylan2d 605 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂)) |
| 5 | 1, 4 | syland 603 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ 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: anim12d 609 ax7 2015 dffi3 9471 cflim2 10303 axpre-sup 11209 xle2add 13301 fzen 13581 rpmulgcd2 16693 pcqmul 16891 sbcie2s 17198 initoeu1 18056 termoeu1 18063 plttr 18387 pospo 18390 lublecllem 18405 latjlej12 18500 latmlem12 18516 hausnei2 23361 uncmp 23411 itgsubst 26090 mpodvdsmulf1o 27237 dvdsmulf1o 27239 2sqlem8a 27469 precsexlem10 28240 axcontlem9 28987 uspgr2wlkeq 29664 shintcli 31348 cvntr 32311 cdj3i 32460 f1resrcmplf1dlem 35100 satffunlem 35406 bj-bary1 37313 heicant 37662 itg2addnc 37681 dihmeetlem1N 41292 modelaxreplem1 44995 fmtnofac2lem 47555 2itscp 48702 mofsn 48753 |
| Copyright terms: Public domain | W3C validator |