![]() |
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 598 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂)) |
5 | 1, 4 | syland 596 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: anim12d 602 ax7 2063 dffi3 8625 cflim2 9420 axpre-sup 10326 xle2add 12401 fzen 12675 rpmulgcd2 15775 pcqmul 15962 initoeu1 17046 termoeu1 17053 plttr 17356 pospo 17359 lublecllem 17374 latjlej12 17453 latmlem12 17469 cygabl 18678 hausnei2 21565 uncmp 21615 itgsubst 24249 dvdsmulf1o 25372 2sqlem8a 25602 axcontlem9 26321 uspgr2wlkeq 26993 shintcli 28760 cvntr 29723 cdj3i 29872 bj-bary1 33760 heicant 34070 itg2addnc 34089 dihmeetlem1N 37444 fmtnofac2lem 42501 2itscp 43517 |
Copyright terms: Public domain | W3C validator |