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 552 | 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 4370 mapen 6708 fival 6826 supelti 6857 supmaxti 6859 infminti 6882 xnegdi 9619 frecuzrdgsuc 10155 hashunlem 10518 2zsupmax 10965 xrmin1inf 11004 serf0 11089 fsumabs 11202 binomlem 11220 cvgratz 11269 efcllemp 11291 ef0lem 11293 tannegap 11362 divalglemnqt 11544 lcmid 11688 hashdvds 11824 ennnfonelemkh 11852 ctinf 11870 setsslid 11936 topbas 12163 tgrest 12265 txss12 12362 cnplimclemle 12733 coseq0q4123 12842 |
Copyright terms: Public domain | W3C validator |