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 606 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜂)) |
5 | 1, 4 | syland 604 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ 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: anim12d 610 ax7 2023 dffi3 8895 cflim2 9685 axpre-sup 10591 xle2add 12653 fzen 12925 rpmulgcd2 16000 pcqmul 16190 initoeu1 17271 termoeu1 17278 plttr 17580 pospo 17583 lublecllem 17598 latjlej12 17677 latmlem12 17693 cygablOLD 19011 hausnei2 21961 uncmp 22011 itgsubst 24646 dvdsmulf1o 25771 2sqlem8a 26001 axcontlem9 26758 uspgr2wlkeq 27427 shintcli 29106 cvntr 30069 cdj3i 30218 f1resrcmplf1dlem 32359 satffunlem 32648 bj-bary1 34596 heicant 34942 itg2addnc 34961 dihmeetlem1N 38441 fmtnofac2lem 43750 2itscp 44788 |
Copyright terms: Public domain | W3C validator |