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 499 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂)) |
5 | 1, 4 | syland 498 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 197 df-an 386 |
This theorem is referenced by: anim12d 586 ax7 1943 dffi3 8337 cflim2 9085 axpre-sup 9990 xle2add 12089 fzen 12358 rpmulgcd2 15370 pcqmul 15558 initoeu1 16661 termoeu1 16668 plttr 16970 pospo 16973 lublecllem 16988 latjlej12 17067 latmlem12 17083 cygabl 18292 hausnei2 21157 uncmp 21206 itgsubst 23812 dvdsmulf1o 24920 2sqlem8a 25150 axcontlem9 25852 uspgr2wlkeq 26542 numclwlk1lem2f1 27227 shintcli 28188 cvntr 29151 cdj3i 29300 bj-bary1 33162 heicant 33444 itg2addnc 33464 dihmeetlem1N 36579 fmtnofac2lem 41480 |
Copyright terms: Public domain | W3C validator |