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 287 | . 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
5 | 4 | ancoms 266 | 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 is referenced by: swopo 4228 opswapg 5025 coexg 5083 iotass 5105 resdif 5389 fvexg 5440 isotr 5717 xpexgALT 6031 ixpssmapg 6622 mapen 6740 mapdom1g 6741 elfir 6861 cauappcvgprlemladdfl 7463 addgt0sr 7583 axmulass 7681 axdistr 7682 negeu 7953 ltaddnegr 8187 nnsub 8759 zltnle 9100 elz2 9122 uzaddcl 9381 qaddcl 9427 xltneg 9619 xleneg 9620 iccneg 9772 uzsubsubfz 9827 fzsplit2 9830 fzss1 9843 uzsplit 9872 fz0fzdiffz0 9907 difelfzle 9911 difelfznle 9912 fzonlt0 9944 fzouzsplit 9956 eluzgtdifelfzo 9974 elfzodifsumelfzo 9978 ssfzo12 10001 qltnle 10023 modfzo0difsn 10168 nn0ennn 10206 ser3mono 10251 iseqf1olemjpcl 10268 iseqf1olemqpcl 10269 fser0const 10289 faclbnd 10487 bcval4 10498 bcpasc 10512 hashfacen 10579 seq3coll 10585 crim 10630 fsumshftm 11214 isumshft 11259 cvgratgt0 11302 mertenslemi1 11304 negdvdsb 11509 dvdsnegb 11510 dvdsmul1 11515 dvdsabseq 11545 dvdsssfz1 11550 odd2np1 11570 ndvdsadd 11628 dvdssqim 11712 nn0seqcvgd 11722 algcvgblem 11730 cncongr2 11785 prmind2 11801 prmdvdsfz 11819 prmndvdsfaclt 11834 resttopon 12340 cnovex 12365 iscn 12366 iscnp 12368 cnco 12390 cndis 12410 hmeoco 12485 bl2in 12572 metss2lem 12666 metss2 12667 bdxmet 12670 metrest 12675 ioo2bl 12712 elcncf 12729 dvexp 12844 supfz 13237 |
Copyright terms: Public domain | W3C validator |