![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl2anr | GIF version |
Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.) |
Ref | Expression |
---|---|
syl2an.1 | ⊢ (𝜑 → 𝜓) |
syl2an.2 | ⊢ (𝜏 → 𝜒) |
syl2an.3 | ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
syl2anr | ⊢ ((𝜏 ∧ 𝜑) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2an.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl2an.2 | . . 3 ⊢ (𝜏 → 𝜒) | |
3 | syl2an.3 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | |
4 | 1, 2, 3 | syl2an 283 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
5 | 4 | ancoms 264 | 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 is referenced by: swopo 4097 opswapg 4871 coexg 4929 iotass 4951 resdif 5223 fvexg 5269 isotr 5535 xpexgALT 5839 mapen 6492 mapdom1g 6493 cauappcvgprlemladdfl 7117 addgt0sr 7224 axmulass 7311 axdistr 7312 negeu 7576 ltaddnegr 7806 nnsub 8354 zltnle 8692 elz2 8714 uzaddcl 8969 qaddcl 9015 xltneg 9193 xleneg 9194 iccneg 9301 uzsubsubfz 9356 fzsplit2 9359 fzss1 9371 uzsplit 9399 fz0fzdiffz0 9432 difelfzle 9436 difelfznle 9437 fzonlt0 9467 fzouzsplit 9479 eluzgtdifelfzo 9497 elfzodifsumelfzo 9501 ssfzo12 9524 qltnle 9546 modfzo0difsn 9691 nn0ennn 9729 isermono 9772 faclbnd 9984 bcval4 9995 bcpasc 10009 hashfacen 10075 crim 10119 negdvdsb 10592 dvdsnegb 10593 dvdsmul1 10598 dvdsabseq 10628 dvdsssfz1 10633 odd2np1 10653 ndvdsadd 10711 dvdssqim 10793 nn0seqcvgd 10803 algcvgblem 10811 cncongr2 10866 prmind2 10882 prmdvdsfz 10900 prmndvdsfaclt 10915 |
Copyright terms: Public domain | W3C validator |