![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl2an2r | GIF version |
Description: syl2anr 284 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
Ref | Expression |
---|---|
syl2an2r.1 | ⊢ (𝜑 → 𝜓) |
syl2an2r.2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
syl2an2r.3 | ⊢ ((𝜓 ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
syl2an2r | ⊢ ((𝜑 ∧ 𝜒) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an2r.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl2an2r.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | |
3 | syl2an2r.3 | . . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏) | |
4 | 1, 2, 3 | syl2an 283 | . 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜒)) → 𝜏) |
5 | 4 | anabss5 545 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: op1stbg 4301 mapen 6560 supelti 6695 supmaxti 6697 infminti 6720 frecuzrdgsuc 9817 hashunlem 10208 2zsupmax 10653 serf0 10737 fsumabs 10855 binomlem 10873 cvgratz 10922 efcllemp 10944 ef0lem 10946 tannegap 11015 divalglemnqt 11194 lcmid 11336 hashdvds 11471 setsidn 11539 |
Copyright terms: Public domain | W3C validator |