Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl2an2r | GIF version |
Description: syl2anr 288 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 287 | . 2 ⊢ ((𝜑 ∧ (𝜑 ∧ 𝜒)) → 𝜏) |
5 | 4 | anabss5 567 | 1 ⊢ ((𝜑 ∧ 𝜒) → 𝜏) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: op1stbg 4400 mapen 6740 fival 6858 supelti 6889 supmaxti 6891 infminti 6914 xnegdi 9651 frecuzrdgsuc 10187 hashunlem 10550 2zsupmax 10997 xrmin1inf 11036 serf0 11121 fsumabs 11234 binomlem 11252 cvgratz 11301 efcllemp 11364 ef0lem 11366 tannegap 11435 divalglemnqt 11617 lcmid 11761 hashdvds 11897 ennnfonelemkh 11925 ctinf 11943 setsslid 12009 topbas 12236 tgrest 12338 txss12 12435 cnplimclemle 12806 coseq0q4123 12915 |
Copyright terms: Public domain | W3C validator |