![]() |
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 4133 opswapg 4917 coexg 4975 iotass 4997 resdif 5275 fvexg 5324 isotr 5595 xpexgALT 5904 mapen 6562 mapdom1g 6563 cauappcvgprlemladdfl 7214 addgt0sr 7321 axmulass 7408 axdistr 7409 negeu 7673 ltaddnegr 7903 nnsub 8461 zltnle 8796 elz2 8818 uzaddcl 9074 qaddcl 9120 xltneg 9298 xleneg 9299 iccneg 9406 uzsubsubfz 9461 fzsplit2 9464 fzss1 9477 uzsplit 9506 fz0fzdiffz0 9541 difelfzle 9545 difelfznle 9546 fzonlt0 9578 fzouzsplit 9590 eluzgtdifelfzo 9608 elfzodifsumelfzo 9612 ssfzo12 9635 qltnle 9657 modfzo0difsn 9802 nn0ennn 9840 isermono 9906 iseqf1olemjpcl 9924 iseqf1olemqpcl 9925 fser0const 9951 faclbnd 10149 bcval4 10160 bcpasc 10174 hashfacen 10241 iseqcoll 10247 crim 10292 fsum3 10779 fsumshftm 10839 isumshft 10884 cvgratgt0 10927 mertenslemi1 10929 negdvdsb 11090 dvdsnegb 11091 dvdsmul1 11096 dvdsabseq 11126 dvdsssfz1 11131 odd2np1 11151 ndvdsadd 11209 dvdssqim 11291 nn0seqcvgd 11301 algcvgblem 11309 cncongr2 11364 prmind2 11380 prmdvdsfz 11398 prmndvdsfaclt 11413 elcncf 11629 supfz 11916 |
Copyright terms: Public domain | W3C validator |